diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-05-15 11:37:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-05-15 11:39:49 +0200 |
| commit | 5d015ae0d90fd7fd3d440acee6ccd501d8b63ba0 (patch) | |
| tree | e73fb685fea3bd4aa5a9eecde1df69c518acccf0 /configure.ml | |
| parent | 76c3b40482978fffca50f6f59e8bcae455680aba (diff) | |
| parent | 3fb81febe8efc34860688cac88a2267cfe298cf7 (diff) | |
Merge v8.5 into trunk
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml index 267d556a2..e21088584 100644 --- a/configure.ml +++ b/configure.ml @@ -1199,7 +1199,9 @@ let write_makefile f = pr "# Defining REVISION\n"; pr "CHECKEDOUT=%s\n\n" vcs; pr "# Option to control compilation and installation of the documentation\n"; - pr "WITHDOC=%s\n" (if withdoc then "all" else "no"); + pr "WITHDOC=%s\n\n" (if withdoc then "all" else "no"); + pr "# Option to produce precompiled files for native_compute\n"; + pr "NATIVECOMPUTE=%s\n" (if !Prefs.nativecompiler then "-native-compiler" else ""); close_out o; Unix.chmod f 0o444 |