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 eb1e307f..8028be1c 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -153,7 +153,7 @@ CVSNAME = ProofGeneral CVSROOT=$(shell cat CVS/Root) # Default emacs for compiling/testing -EMACS=$(shell if [ -z "`which xemacs`"]; then echo emacs; else echo xemacs; fi) +EMACS=$(shell if [ -z "`which xemacs`" ]; then echo emacs; else echo xemacs; fi) # Emacs for batch compiling BATCHEMACS=$(EMACS) -batch -q -no-site-file |