aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-06-24 14:49:48 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-06-27 23:13:14 +0200
commitc9451add699a3e567eefa9de96426b86a4648edd (patch)
tree0b62defb859cc65b956ffe6d040fafb99bc67b1b /tools/coq_makefile.ml
parentccb220a27392ef45b5ef8a8493fdba061c14889b (diff)
Fix off-by-1 bug in coq_makefile
Diffstat (limited to 'tools/coq_makefile.ml')
-rw-r--r--tools/coq_makefile.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 65b2441f7..c86253477 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -141,8 +141,8 @@ let standard opt =
print "\"\n\n"
let classify_files_by_root var files (inc_ml,inc_i,inc_r) =
- if List.exists (fun (pdir,_,_) -> pdir = ".") inc_r
- || List.exists (fun (pdir,_,_) -> pdir = ".") inc_i
+ if List.exists (fun (pdir,_,_) -> pdir = ".") inc_r ||
+ List.exists (fun (pdir,_,_) -> pdir = ".") inc_i
then ()
else
let absdir_of_files =List.rev_map
@@ -207,7 +207,7 @@ let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) =
(fun x -> x^string_of_int i)
in
let pdir' = physical_dir_of_logical_dir ldir in
- (pdir,pdir',vars_r)::out) 1 [] l
+ (pdir,pdir',vars_r)::out) 0 [] l
in (Some varq, other)
let install_include_by_root perms =