diff options
author | Rustan Leino <unknown> | 2015-10-02 14:46:50 -0700 |
---|---|---|
committer | Rustan Leino <unknown> | 2015-10-02 14:46:50 -0700 |
commit | c5a1c58d3c89c55c31331cb419cd3c06e276b5dd (patch) | |
tree | 02a26a0b286acb47733bcf4498b17ae0157341c5 /Test/dafny0 | |
parent | d6d0062d4fd25d733d97e02ea65d9653f7d77175 (diff) |
Fixed latent crash of hovertext/outlining with include.
(This also undoes two previous attempted fixes, which had accidentally disabled some outlining and hovertexts.)
Diffstat (limited to 'Test/dafny0')
0 files changed, 0 insertions, 0 deletions