diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index 01cc4d8780..eeb648ba1e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -272,11 +272,10 @@ endif ## Explicit dependencies for grammar stuff -GRAMBASEDEPS := grammar/gramCompat.cmo grammar/q_util.cmi -GRAMCMO := grammar/gramCompat.cmo grammar/q_util.cmo \ +GRAMBASEDEPS := grammar/q_util.cmi +GRAMCMO := grammar/q_util.cmo \ grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo -grammar/q_util.cmi : grammar/gramCompat.cmo grammar/argextend.cmo : $(GRAMBASEDEPS) grammar/q_util.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo |