diff options
| author | Enrico Tassi | 2017-07-17 18:05:34 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2017-07-20 15:44:13 +0200 |
| commit | ad8bf70ccc61849cfb1ade20ce426ea2ec74aa0e (patch) | |
| tree | 3513182351b72746e870d9e0ecfdce4a1c432c58 /API/API.mllib | |
| parent | 1fd1ca0703811392c890c41a796ed7efdaacca28 (diff) | |
coq-makefile: strip windows drive letter when DESTDIR is not empty
In unix one can concatenate a prefix with an absolute path in
order to obtain a valid path. This is not the case on Windows.
Diffstat (limited to 'API/API.mllib')
0 files changed, 0 insertions, 0 deletions