diff options
| -rw-r--r-- | Makefile.devel | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/Makefile.devel b/Makefile.devel index acb5c434..1676980f 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -152,9 +152,6 @@ CVSNAME = ProofGeneral # make clean in a non cvs directory. CVSROOT=$(shell cat CVS/Root) -# Default emacs for compiling/testing -EMACS=$(shell if [ -z "`which xemacs`" ]; then echo emacs; else echo xemacs; fi) - # Emacs for batch compiling BATCHEMACS=$(EMACS) -batch -q -no-site-file |