allow '#' characters by simply doubling them

LibertyEiffel · Oct 28, 2015 · 668e0fa · 668e0fa
1 parent efceea3
commit 668e0fa
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/lib/string/internal/partially_filled_string.e b/src/lib/string/internal/partially_filled_string.e
@@ -45,6 +45,9 @@ feature {ANY}
                   save_i := i
                   state := 2
                   accu := 0
+               elseif c = '#' then
+                  tagged_out_memory.extend('#')
+                  state := 0
                else
                   tagged_out_memory.extend('#')
                   i := i - 1