aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorRaphaël Monat2017-10-03 16:20:46 +0200
committerRaphaël Monat2017-10-03 16:20:46 +0200
commite664022ba1314d866e4e148d5f5f925654db0487 (patch)
tree0cb2ce6b8d3b4f735d4b2f15f2fd775bfdcd1e61 /lib
parentdfa56fb57b09296cdf311ec5972d2d33b787e48c (diff)
parent2b9a34e2ffb2bf066b3b0f8452e35622519cae1c (diff)
Merge branch 'master' of https://github.com/coq/coq
Diffstat (limited to 'lib')
-rw-r--r--lib/coqProject_file.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 13de731f54..970666638c 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -206,7 +206,7 @@ let rec find_project_file ~from ~projfile_name =
if Sys.file_exists fname then Some fname
else
let newdir = Filename.dirname from in
- if newdir = "" || newdir = "/" then None
+ if newdir = from then None
else find_project_file ~from:newdir ~projfile_name
;;