diff options
| author | Hugo Herbelin | 2019-11-30 15:38:17 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-11-30 15:38:17 +0100 |
| commit | e29a479c5c38ed9318f4443f22ffced860a00792 (patch) | |
| tree | f9b3ed1b02f9e906abcc43bd5284b49a2e4b0e1d /dev/doc | |
| parent | 639886e771882e2c3302cbadc35e9383b34db1fe (diff) | |
coq_makefile: ml4 -> mlg in usage (since ml4 files are rejected).
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions