aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2013-12-09 17:14:55 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2013-12-20 18:40:39 +0100
commitf42ebfc4347e6b5db4aae4ab2b7d02e3b007e732 (patch)
tree2e0a16a594df25480b4e4114f3d38b186c180e41 /Makefile
parent1e32ea82502c9ad8a0046d4dfe326f9a2e035101 (diff)
Remove unused Makefile lines about .elc compilation
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile11
1 files changed, 0 insertions, 11 deletions
diff --git a/Makefile b/Makefile
index 1d235d5b2..8aa76d6a1 100644
--- a/Makefile
+++ b/Makefile
@@ -250,17 +250,6 @@ tags:
etags --append --language=none\
"--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/"
-
-%.elc: %.el
-ifdef COQ_CONFIGURED
- echo "(setq load-path (cons \".\" load-path))" > $*.compile
- echo "(byte-compile-file \"$<\")" >> $*.compile
- - $(EMACS) -batch -l $*.compile
- rm -f $*.compile
-else
- @echo "Please run ./configure first" >&2; exit 1
-endif
-
# Useful to check that the exported variables are within the win32 limits
printenv: