diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-28 11:54:11 +0200 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-28 11:54:11 +0200 |
commit | 2bcb2cb8ddadbaf2e5b6d4abbfdbdf3bc88cc4c6 (patch) | |
tree | 05ee31b54a045a55e786f20b2e9d1c77a9dee7ec /plugins/micromega | |
parent | 8d3c142ec750612b7d02777ff2d6fd5286fb683d (diff) |
Fix incorrect syntax highlighting after the Goal command.
Diffstat (limited to 'plugins/micromega')
0 files changed, 0 insertions, 0 deletions