aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-12-04 09:32:47 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-12-04 09:32:47 +0000
commit74a67eda542bf3ea723e0559131ef97dd753148f (patch)
treef5905edad4a29d21f5950d73eacd65aa18659043 /tools
parentfa4169dbe98db430a572329088743394bd9ea88b (diff)
fichiers DOS
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3371 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/gallina_lexer.mll4
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index 4d05688c3..0dc012b52 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -22,8 +22,8 @@
}
-let space = [' ' '\t' '\n']
-let enddot = '.' (' ' | '\t' | '\n' | eof)
+let space = [' ' '\t' '\n' '\r']
+let enddot = '.' (' ' | '\t' | '\n' | '\r' | eof)
rule action = parse
| "Theorem" space { print "Theorem "; body lexbuf;