diff options
author | 2015-08-16 00:32:23 +0200 | |
---|---|---|
committer | 2015-08-16 03:51:20 +0200 | |
commit | 2c70dd6a256ed4cac2b74bd0c8719ab37fffcb84 (patch) | |
tree | 4d39756908a91c73535628bbb648018799670d1b /ide/config_lexer.mll | |
parent | 2bb05717bde540332aa814a59da3745f2097dedf (diff) |
Simplifying CoqIDE preferences mechanism.
We use a class-based system instead of the old record-based system. This
allows for more uniformity and the possibility to define complex
interactions with preferences based on GTK signals. This will allow to
simplify some architectural choices.
Diffstat (limited to 'ide/config_lexer.mll')
-rw-r--r-- | ide/config_lexer.mll | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index 87cc6d06e..367153568 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -17,7 +17,7 @@ let space = [' ' '\010' '\013' '\009' '\012'] let char = ['A'-'Z' 'a'-'z' '_' '0'-'9'] -let ident = char+ +let ident = (char | '.')+ let ignore = space | ('#' [^ '\n']*) rule prefs m = parse |