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.
 ##