aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-03 15:34:46 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-03 15:34:46 +0200
commit90c4339a54e392b4564c9851fbd48fe910bb4cab (patch)
treedd01d9bbc9ed985d048f1e95fedbe11ba19ff5b3 /lib
parent3a8209d262ef586baee5b76161afd83893d1dad3 (diff)
parent77d95ecd65a6bbebfcd89193fb3e2c43ebc6469a (diff)
Merge PR #1100: Avoid looping when searching for CoqProject.
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 13de731f5..970666638 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
;;