From 3b4b50789e74e7d596199e4b18349a810ae18696 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 6 Oct 2012 11:45:34 +0000 Subject: Turn mltop.ml4 into a regular ocaml file The IFDEF's in mltop.ml4 were there to support platforms with a native ocaml compiler but no dynlink.cmxa, a situation that should be pretty rare in the Coq community nowadays (playing with coqtop on ARM, anyone ?). So we now refuse to build a native coqtop unless dynlink.cmxa exists (cf ./configure), and we explain how to create a dummy one if necessary (cf dev/dynlink.ml). This way, we can clean-up mltop.ml, and remove ugly special rules in Makefile and myocamlbuild NB: I checked that this shouldn't have any impact on Coq's debian packages on exotic architectures (arm, mips, ...), since apparently on these architectures no ocamlopt at all are shipped, and coq packages are already byte-only git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15879 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .gitignore | 3 --- 1 file changed, 3 deletions(-) (limited to '.gitignore') diff --git a/.gitignore b/.gitignore index c3669497f..2b497f9a9 100644 --- a/.gitignore +++ b/.gitignore @@ -136,15 +136,12 @@ tactics/eqdecide.ml tactics/extratactics.ml tactics/extraargs.ml tools/coq_tex.ml -toplevel/mltop.ml toplevel/whelp.ml ide/coqide_main.ml ide/coqide_main_opt.ml # other auto-generated files -toplevel/mltop.optml -toplevel/mltop.byteml kernel/byterun/coq_jumptbl.h kernel/copcodes.ml scripts/tolink.ml -- cgit v1.2.3