diff options
| author | Enrico Tassi | 2017-05-15 11:06:57 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2017-05-23 10:48:28 +0200 |
| commit | 2423f9e58e74dcb2fe9f3ddbbd417e5e1bf1ef24 (patch) | |
| tree | 96f8f3d92a6121704512791a3ccfedf3f6c7c3ba /lib | |
| parent | 3759772965ba91a56f0a6614c192347fd0283edc (diff) | |
coq_makefile: avoid spurious ./ in generated .conf file
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coqProject_file.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 64076d6049..7a16605695 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -105,6 +105,8 @@ let parse f = ;; let process_cmd_line orig_dir proj args = + let orig_dir = (* avoids turning foo.v in ./foo.v *) + if orig_dir = "." then "" else orig_dir in let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in let mk_path d = let p = CUnix.correct_path d orig_dir in |