diff options
| author | Hugo Herbelin | 2019-05-11 16:17:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-14 11:27:15 +0200 |
| commit | df98a88a1e35213e994ec583f6ad4e0d3ccac868 (patch) | |
| tree | fb2fce0e40a14de61299bb98c420b6ed0b800292 /doc/plugin_tutorial/tuto3 | |
| parent | 9a49153b2104e8d7ca0d7789b47299295272746c (diff) | |
CoqIDE: Treat unknown arguments starting with dash as unknown options rather than files.
Diffstat (limited to 'doc/plugin_tutorial/tuto3')
0 files changed, 0 insertions, 0 deletions