aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-11-14 09:59:26 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-11-14 09:59:26 +0000
commit2ad5635db7944c2e31390730f85b2c36d43ec9df (patch)
tree9ac8553b13cad254de4f2653c9e2929ec603aa89 /Makefile
parentaaea65e54a7baa5575f612487df6041cfc807e35 (diff)
Add demoisa dir to makefiles.
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 62d1b0bf..4cc23298 100644
--- a/Makefile
+++ b/Makefile
@@ -15,7 +15,7 @@
###########################################################################
-ELISP_DIRS = generic lego coq isa isar plastic
+ELISP_DIRS = generic lego coq isa isar plastic demoisa
EMACS = xemacs
PWD=$(shell pwd)