aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.devel
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-02-07 18:45:32 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-02-07 18:45:32 +0000
commita368bcd61cd9c8832cd702568889c123b6ea8679 (patch)
treeac9ef6785e80510f9c64dba230a8010f5b67188d /Makefile.devel
parent806ad865a853354dc8ce9aac0ef79844941f4bd0 (diff)
Add Emacs mode tag
Diffstat (limited to 'Makefile.devel')
-rw-r--r--Makefile.devel1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.devel b/Makefile.devel
index a235d310..14ef5573 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -1,3 +1,4 @@
+## -*- makefile -*-
##
## Makefile for Proof General development.
##