From bf69f9e2204de87a08ef2cc622d347b33f3f42ce Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 19 May 2010 15:29:24 +0000 Subject: Remove compile-command pragmas for emacs These declarations (e.g. make -C .. bin/coqtop.byte) are quite annoying when debugging stuff over the whole archive: all of a sudden, M-x recompile isn't doing what you intended just because you've visited some specific files. Instead: - Feel free to rather add intermediate targets in the Makefile if they aren't there yet. - For avoiding typing the -C with many .. after, you can have a look at my recursively-descending make: http://www.pps.jussieu.fr/~letouzey/download/make.sh which is to be renamed make and placed in a bin dir with more priority than /usr/bin. Beware! I've already add a few bad surprises with this hack, but it's really convenient nonetheless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13014 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/funind/merge.ml | 6 ------ plugins/subtac/eterm.ml | 1 - plugins/subtac/subtac_cases.ml | 1 - plugins/subtac/subtac_classes.ml | 1 - plugins/subtac/subtac_coercion.ml | 1 - plugins/subtac/subtac_obligations.ml | 1 - plugins/subtac/subtac_pretyping_F.ml | 1 - 7 files changed, 12 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 26f49f6d49..ccc37046f9 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -1023,9 +1023,3 @@ let relprinctype_to_funprinctype relprinctype nfuns = url = "citeseer.ist.psu.edu/bundy93rippling.html" } *) -(* -*** Local Variables: *** -*** compile-command: "make -C ../.. plugins/funind/merge.cmo" *** -*** indent-tabs-mode: nil *** -*** End: *** -*) diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml index bfa2d47413..9790667c42 100644 --- a/plugins/subtac/eterm.ml +++ b/plugins/subtac/eterm.ml @@ -1,4 +1,3 @@ -(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *) (** - Get types of existentials ; - Flatten dependency tree (prefix order) ; diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 4ec34a91ad..29ce9d3d4a 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -1,4 +1,3 @@ -(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (*