aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CMlexer.mll
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2016-07-11 12:08:32 +0200
committerGitHub <noreply@github.com>2016-07-11 12:08:32 +0200
commitc9cbfda0506dfac791ff58ebb72fe56c333f8ad3 (patch)
tree592be2bddc8f36e22cb7d4c2c1a2ae05ace50ae8 /backend/CMlexer.mll
parent4c7650c3eaf4dfbe5971864bf084e76f844051ee (diff)
parent2ef43e7647ccd65a2a8f1d9fdd067a18e52c39cb (diff)
downloadcompcert-c9cbfda0506dfac791ff58ebb72fe56c333f8ad3.tar.gz
compcert-c9cbfda0506dfac791ff58ebb72fe56c333f8ad3.zip
Merge pull request #105 from m-schmidt/master
Fix parsing and handling of CMinor files
Diffstat (limited to 'backend/CMlexer.mll')
-rw-r--r--backend/CMlexer.mll1
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index c82f5401..65f244b5 100644
--- a/backend/CMlexer.mll
+++ b/backend/CMlexer.mll
@@ -136,6 +136,7 @@ rule token = parse
| "]" { RBRACKET }
| "readonly" { READONLY }
| "return" { RETURN }
+ | "runtime" { RUNTIME }
| ")" { RPAREN }
| ";" { SEMICOLON }
| "/" { SLASH }