diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-19 15:29:24 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-19 15:29:24 +0000 |
| commit | bf69f9e2204de87a08ef2cc622d347b33f3f42ce (patch) | |
| tree | 9d4f62320f85a700bd5079061593949f82b4ddb4 /doc/refman/Setoid.tex | |
| parent | faa0de5c67594980f8ad871dcf71c0dc98865a5e (diff) | |
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
Diffstat (limited to 'doc/refman/Setoid.tex')
| -rw-r--r-- | doc/refman/Setoid.tex | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex index 20c8c02b7..8e1bb10c9 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: |