diff options
| author | Gregory Malecha | 2014-08-01 19:06:00 -0400 |
|---|---|---|
| committer | Pierre Boutillier | 2014-08-25 14:13:24 +0200 |
| commit | d8f73aee76e8b63db97f41e978b579477a82ed50 (patch) | |
| tree | aebec70c9db313beb431d4527445ba97d842ebbb /tools | |
| parent | 6c72e455a048d69048ddf386c43d5fc5eb4597a4 (diff) | |
Make coqdep find Require commands prefixed by Time
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdep_lexer.mll | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 3bfea0c289..7d2978b253 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -90,6 +90,8 @@ rule coq_action = parse { load_file lexbuf } | "Add" space+ "LoadPath" space+ { add_loadpath lexbuf } + | "Time" space+ + { coq_action lexbuf } | space+ { coq_action lexbuf } | "(*" |