diff options
| author | Pierre Letouzey | 2017-03-21 16:13:24 +0100 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:53 -0400 |
| commit | ec0ad20de8daf2ad9f3237de92a745247db845f5 (patch) | |
| tree | 4b43994be9699398ef3182764681d5287a20806b /Makefile.common | |
| parent | 24ccc118ccfb4c1223cd37bd43c9d26a77851176 (diff) | |
remove legacy syntax plugins subsumed by Numeral Notation
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/Makefile.common b/Makefile.common index 4f09fb376a..09457ced7b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -140,10 +140,8 @@ FOCMO:=plugins/firstorder/ground_plugin.cmo CCCMO:=plugins/cc/cc_plugin.cmo BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo -NATSYNTAXCMO:=plugins/syntax/nat_syntax_plugin.cmo -OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \ - positive_syntax_plugin.cmo n_syntax_plugin.cmo \ - z_syntax_plugin.cmo r_syntax_plugin.cmo \ +SYNTAXCMO:=$(addprefix plugins/syntax/, \ + r_syntax_plugin.cmo \ int31_syntax_plugin.cmo \ ascii_syntax_plugin.cmo \ string_syntax_plugin.cmo \ @@ -157,7 +155,7 @@ PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \ $(QUOTECMO) $(RINGCMO) \ $(EXTRACTIONCMO) \ $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ - $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \ + $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \ $(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) ifeq ($(HASNATDYNLINK)-$(BEST),false-opt) |