Merge branch 'master' of github.com:Kappa-Dev/KappaTools

Kappa-Dev · Aug 30, 2023 · 3e5eb6e · 3e5eb6e
2 parents db120ac + 41ddf77
commit 3e5eb6e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/core/grammar/klexer4.mll b/core/grammar/klexer4.mll
@@ -68,7 +68,7 @@ rule token = parse
   | integer as n { INT (int_of_string n) }
   | real as f { FLOAT (float_of_string f) }
   | '\'' ([^'\n' '\'']+ as x) '\''{ LABEL(x) }
-  | '\"' ([^'\n' '\"']+ as x) '\"'{ STRING(x) }
+  | '\"' ([^'\n' '\"']* as x) '\"'{ STRING(x) }
   | '\'' ([^'\n' '\'']+ as s) (eof | '\n')
     { raise (ExceptionDefn.Syntax_Error
       ("Unterminated label: "^s,