diff options
| author | Guillaume Melquiond | 2015-09-16 07:41:03 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-09-16 07:41:03 +0200 |
| commit | 95903cc3bcb9aed92459e644d295be4d9ca25405 (patch) | |
| tree | 2334c41a017b455fb8c8357ca8b02a35196246a0 | |
| parent | 6af9f644b64acf485c1628247f5435d09b990b79 (diff) | |
Change coq_makefile's default from "-Q . Top" to "-R . Top". (Fix bug #3603)
| -rw-r--r-- | tools/coq_makefile.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 934a632dd1..d3374675d2 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -769,7 +769,7 @@ let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((ml_inc,i_inc,r_inc) as l && not_tops mllib && not_tops mlpack) then l else - ((".",here)::ml_inc,(".","Top",here)::i_inc,r_inc) + ((".",here)::ml_inc,i_inc,(".","Top",here)::r_inc) let warn_install_at_root_directory (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_ml,inc_i,inc_r) = |