From 0bba01b9b2fbddb472c8d84d6cc1d7cd3fb24b23 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 4 Mar 2007 13:38:39 +0000
Subject: Choose Emacs instead of XEmacs

---
 Makefile.devel | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'Makefile.devel')

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
 
-- 
cgit v1.2.3