diff options
| author | Maxime Dénès | 2017-06-14 00:11:00 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-14 00:11:00 +0200 |
| commit | 13d23aafe01f87bdbf2205217b82b7836661c5de (patch) | |
| tree | 873a84dbccc56f5d2f53b3a70161b25b6ac4a676 /Makefile.common | |
| parent | 25462addaf604ff51e886bbc92937bb272982b04 (diff) | |
| parent | 268ccbb0d3d990e42cef4ae4833e0e7964aea24d (diff) | |
Merge PR#498: Bignums as a separate opam package
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/Makefile.common b/Makefile.common index b2e1d47dfd..ec5e6ac855 100644 --- a/Makefile.common +++ b/Makefile.common @@ -129,8 +129,8 @@ RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo NATSYNTAXCMO:=plugins/syntax/nat_syntax_plugin.cmo OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \ z_syntax_plugin.cmo \ - numbers_syntax_plugin.cmo \ r_syntax_plugin.cmo \ + int31_syntax_plugin.cmo \ ascii_syntax_plugin.cmo \ string_syntax_plugin.cmo ) DERIVECMO:=plugins/derive/derive_plugin.cmo @@ -161,14 +161,8 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx) # vo files ########################################################################### -GENVOFILES := $(GENVFILES:.v=.vo) - -THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v")) \ - $(filter theories/%, $(GENVOFILES)) - -PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v")) \ - $(filter plugins/%, $(GENVOFILES)) - +THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v")) +PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v")) ALLVO := $(THEORIESVO) $(PLUGINSVO) VFILES := $(ALLVO:.vo=.v) |