diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2007-03-04 13:38:39 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2007-03-04 13:38:39 +0000 |
| commit | 0bba01b9b2fbddb472c8d84d6cc1d7cd3fb24b23 (patch) | |
| tree | adbdcec220fa61ee5959c964bc86de0f43c6a94d /Makefile.devel | |
| parent | 365deef3a6fac0821e81ae691b92f2af386611d9 (diff) | |
Choose Emacs instead of XEmacs
Diffstat (limited to 'Makefile.devel')
| -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 |