diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-06-13 11:08:05 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-06-13 11:08:05 +0200 |
| commit | c7059c8f4e880f2b7f1ee895e0d4d32eee2f36fd (patch) | |
| tree | 35ff45b459138ac57785e0cc8bf263c5c49a4a37 /hol-light | |
| parent | 889069bc593bb9a857372783ff837b13e64942d6 (diff) | |
Fix the fix #355.
The fix was bad: no ore hyps were foldable/highlightable.
Diffstat (limited to 'hol-light')
0 files changed, 0 insertions, 0 deletions