diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-04 19:47:18 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-23 02:35:58 +0100 |
| commit | 19a584d3fa9594abdf3dcc0148f368547ce77ccc (patch) | |
| tree | 4888e4e7fe950382c6e635e9854d9d1790527fdd /lib/profile.ml | |
| parent | 143244e0606a790b73da2360fb0eabe3d98d4b4e (diff) | |
Forbidding -o and -f in input file of coq_makefile.
This was apparently either silently doing nothing or failing.
Diffstat (limited to 'lib/profile.ml')
0 files changed, 0 insertions, 0 deletions