diff options
| author | Hugo Herbelin | 2019-05-08 21:26:37 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 02:31:27 +0200 |
| commit | cc9a10182255527959fc10bd86f18a7b40ef5a2a (patch) | |
| tree | 4b6832513ca210fd8ffbe9ab694abf7aec655e83 /lib | |
| parent | 01c965e1989cbc528d46b1751d8c2c708542da4e (diff) | |
Removing -filterops "hack" from coqtop.
This is now the "coqidetop" binary which specifically know how to
collect extra arguments.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions