diff options
| author | Niklas Haas <git@nand.wakku.to> | 2014-03-12 10:31:31 +0100 |
|---|---|---|
| committer | Mateusz Kowalczyk <fuuzetsu@fuuzetsu.co.uk> | 2014-03-13 19:18:06 +0000 |
| commit | 3606ad5fdb8b9c2c3f9a62de1d26702ad41f9a10 (patch) | |
| tree | 56e35153453b6469ef34cd356b966293ee81d1ff /resources/html/Ocean.std-theme | |
| parent | 8f71c6f26eb5b36e5a1ca253b8c8ffdca75849d8 (diff) | |
Hide RHS of TFs with non-exported right hand sides
Not sure what to do about data families yet, since technically it would
not make a lot of sense to display constructors that cannot be used by
the user.
Diffstat (limited to 'resources/html/Ocean.std-theme')
0 files changed, 0 insertions, 0 deletions