# HG changeset patch
# User wenzelm
# Date 1300910825 -3600
# Node ID 71662f36b57306c32b401b314090ecef3aac0ad8
# Parent  d5bf0ce40bd7374fd88e9649c205a5d3ccff71c5
added editor mode line;

diff -r d5bf0ce40bd7 -r 71662f36b573 src/HOL/Tools/Nitpick/etc/settings
--- a/src/HOL/Tools/Nitpick/etc/settings	Wed Mar 23 20:57:37 2011 +0100
+++ b/src/HOL/Tools/Nitpick/etc/settings	Wed Mar 23 21:07:05 2011 +0100
@@ -1,1 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"