diff options
| author | Enrico Tassi | 2019-12-01 17:38:49 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-12-01 17:38:49 +0100 |
| commit | c0d116209fdda0858b182000a19ebfeacd2b1b83 (patch) | |
| tree | f9b3ed1b02f9e906abcc43bd5284b49a2e4b0e1d /dev/tools/pre-commit | |
| parent | 639886e771882e2c3302cbadc35e9383b34db1fe (diff) | |
| parent | e29a479c5c38ed9318f4443f22ffced860a00792 (diff) | |
Merge PR #11220: coq_makefile: ml4 -> mlg in usage (since ml4 files are rejected).
Reviewed-by: gares
Diffstat (limited to 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions