# HG changeset patch
# User wenzelm
# Date 1468238190 -7200
# Node ID 5ad98525e918f3e485132b8a58d3dee45b0aeedb
# Parent  9974230f95745fb02a1f14ec6dec80cb584998ad
more robust;

diff -r 9974230f9574 -r 5ad98525e918 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 11:16:10 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 13:56:30 2016 +0200
@@ -121,7 +121,7 @@
             }
 
           actions.clear()
-          actions.add(new IndentAction.AlignOffset(indent))
+          actions.add(new IndentAction.AlignOffset(indent max 0))
         case _ =>
       }
     }