diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-08 15:13:13 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-08 15:15:06 +0200 |
| commit | f6ce65b4d49f0a3a3af7e0e7811934136f59943c (patch) | |
| tree | d7b48be2926891e20890eed4384dd42e1c110bb1 /grammar | |
| parent | d060577f274658dd8189fceb92316b3cd37417b9 (diff) | |
remove grammar/grammar.mllib
grammar.cma is built by Makefile.build in a specific, hardcoded way.
Let's remove this old .mllib file to avoid potential confusions in
the future.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/grammar.mllib | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib deleted file mode 100644 index 6c3ce7f03..000000000 --- a/grammar/grammar.mllib +++ /dev/null @@ -1,5 +0,0 @@ -GramCompat -Q_util -Argextend -Tacextend -Vernacextend |