diff options
| author | Pierre Courtieu | 2015-11-06 17:04:24 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2015-11-06 18:55:36 +0100 |
| commit | a8b248096e5120f58157b0fc3bd06ca07118a8ab (patch) | |
| tree | 83d2ba588e3ffcf0b7223bad42866ce623ac85aa /dev/base_include | |
| parent | 76bc7f9d164c20583c6561127bf36e7247a37c6b (diff) | |
Fixing #4406 coqdep: No recursive search of ml (-I).
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions