diff options
| author | Hugo Herbelin | 2014-12-04 08:45:07 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-04 11:39:12 +0100 |
| commit | 21a1c8abdd5807427849c34875c294cb6ad7d899 (patch) | |
| tree | 3a722cc770663196bb23ad37c36bd23fff1a41bd /dev/include | |
| parent | 34bb77c953e917f5fbff489c5758abcbadc22224 (diff) | |
coqdep: Warning about ml file clashes, keeping the file corresponding
to the first -I option.
Fortunately, with -I option, only one file can be found by occurrence
of the option, so on the contrary of -Q/-R options for v files, the
order is not file-system dependent.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions