diff options
| author | Pierre Roux | 2019-02-20 18:00:04 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:51 +0100 |
| commit | 6133877fc097412233a60740fdf94374abb79559 (patch) | |
| tree | 26655b276f177cc77f108524278eb620e03c97c1 /Makefile.build | |
| parent | f0bf1511e59e528e090a87cfcc220f93c2431ecd (diff) | |
Add primitive floats to checker
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index ed4cde2b16..f9286c9635 100644 --- a/Makefile.build +++ b/Makefile.build @@ -566,7 +566,7 @@ $(FAKEIDEBYTE): $(FAKEIDECMO) | $(IDETOPBYTE) # votour: a small vo explorer (based on the checker) -VOTOURCMO:=clib/cObj.cmo kernel/uint63.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo +VOTOURCMO:=clib/cObj.cmo kernel/uint63.cmo kernel/float64.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo bin/votour: $(call bestobj, $(VOTOURCMO)) $(SHOW)'OCAMLBEST -o $@' |