From f42ebfc4347e6b5db4aae4ab2b7d02e3b007e732 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 9 Dec 2013 17:14:55 +0100
Subject: Remove unused Makefile lines about .elc compilation

---
 Makefile | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 1d235d5b23..8aa76d6a1e 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:
-- 
cgit v1.2.3