diff options
| author | David Aspinall | 2006-08-23 17:19:47 +0000 |
|---|---|---|
| committer | David Aspinall | 2006-08-23 17:19:47 +0000 |
| commit | e0145fc17a0d7a649995962dbc66f0122bdfecc6 (patch) | |
| tree | b079246162b569a997ae5be9b624ea8a6507091b | |
| parent | f10621fce14c44b8d776cdf1abb9998767fceec1 (diff) | |
Syntax strictitude
| -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 |