lib/browser/GraphBrowser/Console.java
changeset 50473 ca4088bf8365
parent 33686 8e33ca8832b1
--- a/lib/browser/GraphBrowser/Console.java	Mon Dec 10 21:55:57 2012 +0100
+++ b/lib/browser/GraphBrowser/Console.java	Tue Dec 11 10:35:42 2012 +0100
@@ -1,6 +1,7 @@
 /***************************************************************************
   Title:      GraphBrowser/Console.java
   Author:     Gerwin Klein, TU Muenchen
+  Options:    :tabSize=2:
 
   This is the graph browser's main class when run as a console application.
   It duplicates some logic from GraphBrowser and GraphView.