From 2423f9e58e74dcb2fe9f3ddbbd417e5e1bf1ef24 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 15 May 2017 11:06:57 +0200
Subject: coq_makefile: avoid spurious ./ in generated .conf file

---
 lib/coqProject_file.ml4 | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib')

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
-- 
cgit v1.2.3