# HG changeset patch
# User wenzelm
# Date 1281037220 -7200
# Node ID e669779bb8c4cb669dc50ca0d574d6ff02dd6403
# Parent  343cb5d4034aeaa375657c1c55d9638a25ec3f06
editor mode;

diff -r 343cb5d4034a -r e669779bb8c4 src/Tools/jEdit/dist-template/etc/settings
--- a/src/Tools/jEdit/dist-template/etc/settings	Thu Aug 05 18:17:59 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/settings	Thu Aug 05 21:40:20 2010 +0200
@@ -1,3 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
 JEDIT_HOME="$COMPONENT"
 JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"