diff options
Diffstat (limited to 'Makefile.devel')
-rw-r--r-- | Makefile.devel | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.devel b/Makefile.devel index 56c17d22..953b9ab9 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -212,7 +212,7 @@ SUBDIRS=$(ELISP_DIRS) etc doc images PWD=$(shell pwd) -BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (list "$(PWD)/generic" "$(PWD)/lib" "$(PWD)/lego" "$(PWD)/coq" "$(PWD)/isa" "$(PWD)/isar") load-path))' -f batch-byte-compile +BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (list "$(PWD)/generic" "$(PWD)/lib" "$(PWD)/lego" "$(PWD)/coq" "$(PWD)/isar") load-path))' -f batch-byte-compile EL=$(shell for f in $(ELISP_DIRS); do ls $$f/*.el; done) ELC=$(EL:.el=.elc) |