diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-31 13:33:01 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-31 13:33:01 +0200 |
commit | 27dffdea5b46f6282c1584db0555213e744352fa (patch) | |
tree | 3f89cd9e8828f1ca1c8a1c10d74f020dcb7543f1 /dev/printers.mllib | |
parent | cb31cd671a0ef4da0cf834dad5b67776098bb0d1 (diff) |
Revert "Rename Lexer -> CLexer."
This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e.
Diffstat (limited to 'dev/printers.mllib')
-rw-r--r-- | dev/printers.mllib | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index e054c1bc7..ad9a5d75e 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -151,7 +151,7 @@ States Genprint Tok -CLexer +Lexer Ppextend Pputils Ppannotation |