summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorThomas Bauereiss2018-12-23 13:55:46 +0100
committerThomas Bauereiss2018-12-23 13:55:46 +0100
commitf70f187dbf667df5e8610978e928d9ba76af8e0e (patch)
tree0be660530a1d0ea4b382e00e7bb697b47b2e7f81 /src
parent8dbe18b8976e30fa88814542ea913ddc4193cd8b (diff)
Remove a comment that breaks Isabelle build
With the new comment syntax, Isabelle seems to barf on that comment, apparently due to the backslashes.
Diffstat (limited to 'src')
-rw-r--r--src/gen_lib/sail2_string.lem4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/gen_lib/sail2_string.lem b/src/gen_lib/sail2_string.lem
index de7588dc..33a665a0 100644
--- a/src/gen_lib/sail2_string.lem
+++ b/src/gen_lib/sail2_string.lem
@@ -64,10 +64,6 @@ let rec n_leading_spaces s =
| _ -> 0
end
else
- (* match len with
- * (\* | 0 -> 0 *\)
- * (\* | 1 -> *\)
- * | len -> *)
(* Isabelle generation for pattern matching on characters
is currently broken, so use an if-expression *)
if nth s 0 = #' '