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
---
 doc/refman/Setoid.tex | 1 -
 1 file changed, 1 deletion(-)

(limited to 'doc/refman')

diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 20c8c02b79..8e1bb10c9b 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -710,5 +710,4 @@ using the command \texttt{Typeclasses Opaque} (see \S \ref{TypeclassesTransparen
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
-%%% compile-command: "make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
 %%% End: 
-- 
cgit v1.2.3