diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2013-11-30 11:04:10 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2013-12-20 18:57:08 +0100 |
commit | 8ba7983f467a6e235ba88e10be90381c9429cad2 (patch) | |
tree | 57d30e939d0e366d59809d3d335fb767cc4d5e91 /ide/preferences.mli | |
parent | d1824e8e6f472385d790c52792c7bf4a5adde41d (diff) |
configure.ml: our configure script is now written in ML :-)
configure is now just a minimal wrapper around the new configure.ml.
This configure.ml is runned with the same ocaml used during
compilation, and starts with a #load "unix.cma".
For now, this new configure script is meant to be 99% compatible
with the old one. Known incompatibilities : the --foo option format
(with two --) isn't supported anymore, use -foo options instead.
Let me know if you encounter any other changes.
Internals:
- We use our own "run" command (based on Unix.create_process) to avoid
relying on some specific shell (/bin/sh or cmd.exe).
- We should have far less issues with filename quoting under windows
since we almost never rely on (cygwin) shell anymore. This remains
to be fully tested, though.
- dev/ocamldebug-coq is slightly different now, to ease its generation
Diffstat (limited to 'ide/preferences.mli')
0 files changed, 0 insertions, 0 deletions