From 00a8604d89f47c903fc5283eebdda67c87468699 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 31 Oct 2018 15:29:57 +0100 Subject: Select OS specific coqide code with cp. --- .gitignore | 2 +- Makefile | 2 +- Makefile.ide | 12 ++-- ide/coqide_QUARTZ.ml.in | 37 +++++++++++ ide/coqide_WIN32.ml.in | 50 +++++++++++++++ ide/coqide_X11.ml.in | 11 ++++ ide/coqide_main.ml | 72 +++++++++++++++++++++ ide/coqide_main.ml4 | 154 --------------------------------------------- ide/coqide_os_specific.mli | 11 ++++ ide/dune | 6 +- 10 files changed, 192 insertions(+), 165 deletions(-) create mode 100644 ide/coqide_QUARTZ.ml.in create mode 100644 ide/coqide_WIN32.ml.in create mode 100644 ide/coqide_X11.ml.in create mode 100644 ide/coqide_main.ml delete mode 100644 ide/coqide_main.ml4 create mode 100644 ide/coqide_os_specific.mli diff --git a/.gitignore b/.gitignore index 709e87cc9c..f9e43a0eb7 100644 --- a/.gitignore +++ b/.gitignore @@ -139,7 +139,7 @@ plugins/ltac/coretactics.ml plugins/ltac/extratactics.ml plugins/ltac/extraargs.ml plugins/ltac/profile_ltac_tactics.ml -ide/coqide_main.ml +ide/coqide_os_specific.ml plugins/ssrmatching/ssrmatching.ml plugins/ssr/ssrparser.ml plugins/ssr/ssrvernac.ml diff --git a/Makefile b/Makefile index f2dc6d7750..b9d8bf34e3 100644 --- a/Makefile +++ b/Makefile @@ -96,7 +96,7 @@ EXISTINGMLI := $(call find, '*.mli') GENML4FILES:= $(ML4FILES:.ml4=.ml) GENMLGFILES:= $(MLGFILES:.mlg=.ml) -export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) kernel/copcodes.ml +export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) diff --git a/Makefile.ide b/Makefile.ide index 6c069a1e50..39af1f8545 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -49,8 +49,8 @@ IDETOPEXE=bin/coqidetop$(EXE) IDETOP=bin/coqidetop.opt$(EXE) IDETOPBYTE=bin/coqidetop.byte$(EXE) -LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.mli ide/coqide_main.ml -LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.mli ide/coqide_main.ml +LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_os_specific.cmo ide/coqide_main.mli ide/coqide_main.ml +LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_os_specific.cmx ide/coqide_main.mli ide/coqide_main.ml IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map @@ -110,10 +110,10 @@ $(COQIDEBYTE): $(LINKIDE) $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \ -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS) $(IDECDEPSFLAGS) $^ -ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp5deps here - $(SHOW)'CAMLP5O $<' - $(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) $(CAMLP5USE) -D$(IDEINT) -impl $< -o $@ - +ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile + @rm -f $@ + cp $< $@ + @chmod -w $@ ide/%.cmi: ide/%.mli $(SHOW)'OCAMLC $<' diff --git a/ide/coqide_QUARTZ.ml.in b/ide/coqide_QUARTZ.ml.in new file mode 100644 index 0000000000..a08bac5772 --- /dev/null +++ b/ide/coqide_QUARTZ.ml.in @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Coqide.do_load x; true) + in + let _ = osx#connect#ns_application_block_termination + ~callback:Coqide.forbid_quit + in + let _ = osx#connect#ns_application_will_terminate + ~callback:Coqide.close_and_quit + in () + +let init () = + let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication + (GtkMenu.MenuShell.cast + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) + in + let () = GtkosxApplication.Application.insert_app_menu_item + osx#as_osxapplication + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 + in + let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication + (Some (GtkMenu.MenuItem.cast + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) + in + osx#ready () diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in new file mode 100644 index 0000000000..8c4649fc39 --- /dev/null +++ b/ide/coqide_WIN32.ml.in @@ -0,0 +1,50 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* "")) + +(* On win32, since coqide is now console-free, we re-route stdout/stderr + to avoid Sys_error if someone writes to them. We write to a pipe which + is never read (by default) or to a temp log file (when in debug mode). +*) + +let reroute_stdout_stderr () = + (* We anticipate a bit the argument parsing and look for -debug *) + let debug = List.mem "-debug" (Array.to_list Sys.argv) in + Minilib.debug := debug; + let out_descr = + if debug then + let (name,chan) = Filename.open_temp_file "coqide_" ".log" in + Coqide.logfile := Some name; + Unix.descr_of_out_channel chan + else + snd (Unix.pipe ()) + in + Unix.set_close_on_exec out_descr; + Unix.dup2 out_descr Unix.stdout; + Unix.dup2 out_descr Unix.stderr + +(* We also provide specific kill and interrupt functions. *) + +external win32_kill : int -> unit = "win32_kill" +external win32_interrupt : int -> unit = "win32_interrupt" +let () = + Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; + set_win32_path (); + Coq.interrupter := win32_interrupt; + reroute_stdout_stderr () + +let init () = () diff --git a/ide/coqide_X11.ml.in b/ide/coqide_X11.ml.in new file mode 100644 index 0000000000..6a5784eac3 --- /dev/null +++ b/ide/coqide_X11.ml.in @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* 0 in + if level_is `ERROR then `FATAL + else if level_is `CRITICAL then `ERROR + else if level_is `DEBUG then `DEBUG + else if level_is `WARNING then `WARNING + else if level_is `MESSAGE then `NOTICE + else `INFO + in + let handler ~level msg = + let header = "Coqide internal error: " in + match log_level level with + |`FATAL -> + let () = GToolbox.message_box ~title:"Error" (header ^ msg) in + Coqide.crash_save 1 + |`ERROR -> + if !Flags.debug then GToolbox.message_box ~title:"Error" (header ^ msg) + else Printf.eprintf "%s\n" (header ^ msg) + |`DEBUG -> Minilib.log msg + |level when Sys.os_type = "Win32" -> Minilib.log ~level msg + |_ -> Printf.eprintf "%s\n" msg + in + let catch domain = + ignore (Glib.Message.set_log_handler ~domain ~levels:all_levels handler) + in + List.iter catch ["GLib";"Gtk";"Gdk";"Pango"] + +let () = catch_gtk_messages () + +let load_prefs () = + try Preferences.load_pref () + with e -> Ideutils.flash_info + ("Could not load preferences ("^Printexc.to_string e^").") + +let () = + load_prefs (); + let argl = List.tl (Array.to_list Sys.argv) in + let argl = Coqide.read_coqide_args argl in + let files = Coq.filter_coq_opts argl in + let args = List.filter (fun x -> not (List.mem x files)) argl in + Coq.check_connection args; + Coqide.sup_args := args; + Coqide.main files; + Coqide_os_specific.init (); + try + GMain.main (); + failwith "Gtk loop ended" + with e -> + Minilib.log ("CoqIde unexpected error:" ^ Printexc.to_string e); + Coqide.crash_save 127 diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 deleted file mode 100644 index 3a92e1bc91..0000000000 --- a/ide/coqide_main.ml4 +++ /dev/null @@ -1,154 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 0 in - if level_is `ERROR then `FATAL - else if level_is `CRITICAL then `ERROR - else if level_is `DEBUG then `DEBUG - else if level_is `WARNING then `WARNING - else if level_is `MESSAGE then `NOTICE - else `INFO - in - let handler ~level msg = - let header = "Coqide internal error: " in - match log_level level with - |`FATAL -> - let () = GToolbox.message_box ~title:"Error" (header ^ msg) in - Coqide.crash_save 1 - |`ERROR -> - if !Flags.debug then GToolbox.message_box ~title:"Error" (header ^ msg) - else Printf.eprintf "%s\n" (header ^ msg) - |`DEBUG -> Minilib.log msg - |level when Sys.os_type = "Win32" -> Minilib.log ~level msg - |_ -> Printf.eprintf "%s\n" msg - in - let catch domain = - ignore (Glib.Message.set_log_handler ~domain ~levels:all_levels handler) - in - List.iter catch ["GLib";"Gtk";"Gdk";"Pango"] - -let () = catch_gtk_messages () - - - -(** System-dependent settings *) - -let os_specific_init () = () - -(** Win32 *) - -IFDEF WIN32 THEN - -(* On win32, we add the directory of coqide to the PATH at launch-time - (this used to be done in a .bat script). *) - -let set_win32_path () = - Unix.putenv "PATH" - (Filename.dirname Sys.executable_name ^ ";" ^ - (try Sys.getenv "PATH" with _ -> "")) - -(* On win32, since coqide is now console-free, we re-route stdout/stderr - to avoid Sys_error if someone writes to them. We write to a pipe which - is never read (by default) or to a temp log file (when in debug mode). -*) - -let reroute_stdout_stderr () = - (* We anticipate a bit the argument parsing and look for -debug *) - let debug = List.mem "-debug" (Array.to_list Sys.argv) in - Minilib.debug := debug; - let out_descr = - if debug then - let (name,chan) = Filename.open_temp_file "coqide_" ".log" in - Coqide.logfile := Some name; - Unix.descr_of_out_channel chan - else - snd (Unix.pipe ()) - in - Unix.set_close_on_exec out_descr; - Unix.dup2 out_descr Unix.stdout; - Unix.dup2 out_descr Unix.stderr - -(* We also provide specific kill and interrupt functions. *) - -external win32_kill : int -> unit = "win32_kill" -external win32_interrupt : int -> unit = "win32_interrupt" -let () = - Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; - set_win32_path (); - Coq.interrupter := win32_interrupt; - reroute_stdout_stderr () -END - -(** MacOSX *) - -IFDEF QUARTZ THEN -let osx = GosxApplication.osxapplication () - -let () = - let _ = osx#connect#ns_application_open_file - ~callback:(fun x -> Coqide.do_load x; true) - in - let _ = osx#connect#ns_application_block_termination - ~callback:Coqide.forbid_quit - in - let _ = osx#connect#ns_application_will_terminate - ~callback:Coqide.close_and_quit - in () - -let os_specific_init () = - let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication - (GtkMenu.MenuShell.cast - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) - in - let () = GtkosxApplication.Application.insert_app_menu_item - osx#as_osxapplication - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 - in - let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication - (Some (GtkMenu.MenuItem.cast - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) - in - osx#ready () -END - -let load_prefs () = - try Preferences.load_pref () - with e -> Ideutils.flash_info - ("Could not load preferences ("^Printexc.to_string e^").") - -let () = - load_prefs (); - let argl = List.tl (Array.to_list Sys.argv) in - let argl = Coqide.read_coqide_args argl in - let files = Coq.filter_coq_opts argl in - let args = List.filter (fun x -> not (List.mem x files)) argl in - Coq.check_connection args; - Coqide.sup_args := args; - Coqide.main files; - os_specific_init (); - try - GMain.main (); - failwith "Gtk loop ended" - with e -> - Minilib.log ("CoqIde unexpected error:" ^ Printexc.to_string e); - Coqide.crash_save 127 diff --git a/ide/coqide_os_specific.mli b/ide/coqide_os_specific.mli new file mode 100644 index 0000000000..ebd09099f0 --- /dev/null +++ b/ide/coqide_os_specific.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* unit diff --git a/ide/dune b/ide/dune index 70a1709f37..5714b1370e 100644 --- a/ide/dune +++ b/ide/dune @@ -33,9 +33,9 @@ (libraries coqide-server.protocol coqide-server.core lablgtk2.sourceview2)) (rule - (targets coqide_main.ml) - (deps (:ml4-file coqide_main.ml4)) - (action (run coqmlp5 -loc loc -impl %{ml4-file} -o %{targets}))) + (targets coqide_os_specific.ml) + (deps (:in-file coqide_X11.ml.in)) ; TODO support others + (action (run cp %{in-file} %{targets}))) (executable (name coqide_main) -- cgit v1.2.3 From e06875ccc11c52b9b9526858c18358a9c4588099 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 29 Oct 2018 14:00:58 +0100 Subject: Remove ml4 from Coq's make build system --- Makefile | 28 +++++++++++----------------- Makefile.build | 14 +++++--------- dev/tools/change-header | 2 +- 3 files changed, 17 insertions(+), 27 deletions(-) diff --git a/Makefile b/Makefile index b9d8bf34e3..e0ab169eda 100644 --- a/Makefile +++ b/Makefile @@ -78,7 +78,6 @@ LEXFILES := $(call find, '*.mll') YACCFILES := $(call find, '*.mly') export MLLIBFILES := $(call find, '*.mllib') export MLPACKFILES := $(call find, '*.mlpack') -export ML4FILES := $(call find, '*.ml4') export MLGFILES := $(call find, '*.mlg') export CFILES := $(call findindir, 'kernel/byterun', '*.c') @@ -94,19 +93,14 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated -GENML4FILES:= $(ML4FILES:.ml4=.ml) GENMLGFILES:= $(MLGFILES:.mlg=.ml) -export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml +export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) -# NB: all files in $(GENFILES) can be created initially, while -# .ml files in $(GENML4FILES) might need some intermediate building. -# That's why we keep $(GENML4FILES) out of $(GENFILES) - ## More complex file lists -export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES) $(GENMLGFILES), $(EXISTINGML)) +export MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML)) export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) include Makefile.common @@ -194,7 +188,7 @@ META.coq: META.coq.in # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean alienclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean clean: objclean cruftclean depclean docclean camldevfilesclean @@ -202,7 +196,7 @@ cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean objclean: archclean indepclean -cruftclean: ml4clean +cruftclean: mlgclean find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} + rm -f gmon.out core @@ -252,8 +246,8 @@ clean-ide: rm -f ide/utf8_convert.ml rm -rf $(COQIDEAPP) -ml4clean: - rm -f $(GENML4FILES) $(GENMLGFILES) +mlgclean: + rm -f $(GENMLGFILES) depclean: find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} + @@ -286,7 +280,7 @@ KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') -KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \ +KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \ $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ $(MLIFILES:.mli=.cmi) \ @@ -308,7 +302,7 @@ include Makefile.ci .PHONY: tags printenv tags: - echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \ + echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ etags --language=none\ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ @@ -317,12 +311,12 @@ tags: "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ "--regex=/module[ \t]+\([^ \t]+\)/\1/" - echo $(ML4FILES) | sort -r | xargs \ + echo $(MLGFILES) | sort -r | xargs \ etags --append --language=none\ "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" checker-tags: - echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \ + echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ etags --language=none\ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ @@ -331,7 +325,7 @@ checker-tags: "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ "--regex=/module[ \t]+\([^ \t]+\)/\1/" - echo $(ML4FILES) | sort -r | xargs \ + echo $(MLGFILES) | sort -r | xargs \ etags --append --language=none\ "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" diff --git a/Makefile.build b/Makefile.build index 08863014ea..fb84a131c7 100644 --- a/Makefile.build +++ b/Makefile.build @@ -86,7 +86,7 @@ byte: coqbyte coqide-byte pluginsbyte printers # This list of ml files used to be in the main Makefile, we moved it here # to avoid exhausting the variable env in Win32 -MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml) +MLFILES := $(MLSTATICFILES) $(GENMLFILES) include Makefile.common include Makefile.vofiles @@ -148,7 +148,7 @@ endif # This include below will lauch the build of all .d. # The - at front is for disabling warnings about currently missing ones. # For creating the missing .d, make will recursively build things like -# coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d). +# coqdep_boot (for the .v.d files) or coqpp (for .mlg -> .ml -> .ml.d). VDFILE := .vfiles MLDFILE := .mlfiles @@ -166,7 +166,7 @@ DEPENDENCIES := \ # of include, and they will then be automatically deleted, leading to an # infinite loop. -.SECONDARY: $(DEPENDENCIES) $(GENFILES) $(ML4FILES:.ml4=.ml) +.SECONDARY: $(DEPENDENCIES) $(GENFILES) $(MLGFILES:.mlg=.ml) ########################################################################### # Compilation options @@ -259,6 +259,7 @@ CAMLP5DEPS:=grammar/grammar.cma CAMLP5USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) +# XXX unused but should be used for mlp files # Main packages linked by Coq. SYSMOD:=-package num,str,unix,dynlink,threads @@ -768,11 +769,6 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50 $(SHOW)'OCAMLYACC $<' $(HIDE)$(OCAMLYACC) --strict "$*.mly" -%.ml: %.ml4 $(CAMLP5DEPS) $(COQPP) - $(SHOW)'CAMLP5O $<' - $(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) \ - $(CAMLP5DEPS) $(CAMLP5USE) $(CAMLP5COMPAT) -impl $< -o $@ - %.ml: %.mlg $(COQPP) $(SHOW)'COQPP $<' $(HIDE)$(COQPP) $< @@ -782,7 +778,7 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50 ########################################################################### # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12) -OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack +OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .mlpack MAINMLFILES := $(filter-out checker/% plugins/%, $(MLFILES) $(MLIFILES)) MAINMLLIBFILES := $(filter-out checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES)) diff --git a/dev/tools/change-header b/dev/tools/change-header index 61cc866602..687c02f4f1 100755 --- a/dev/tools/change-header +++ b/dev/tools/change-header @@ -22,7 +22,7 @@ lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)' modified=0 kept=0 -for i in `find . -name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do +for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do headline=`head -n 1 $i` if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then # Has emacs header -- cgit v1.2.3