diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-29 12:12:53 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-29 13:17:19 +0200 |
commit | dd134de0b068c70adb80c94921673086f0002c30 (patch) | |
tree | 9a482d44a6c031b14b1f2929da337e23828a3885 /Makefile.build | |
parent | ff820359e7adb4a414f4796e342f43b5264580a5 (diff) |
coq_makefile : do not build bytecode versions of plugins by default
make install does not install these *.cm(o|a) files either.
You could always do manually :
- make bytefiles : to build the bytecode *.cm(o|a) files
- make install-byte : to install these files
- make byte : to compile the whole development with the bytecode version
of Coq (this builds the *.cm(o|a) files, but also the .vo via coqc -byte).
Technically, the behavior of make is controlled by the OPT variable,
which could be -byte or -opt. For instance, 'make byte' corresponds to a
'make OPT:=-byte'
Note that coqdep is used with the new option "-dyndep var" : when seeing
a Declare ML Module "foo", "coqdep -dyndep var" does not decide whether to
depend on foo.cma or foo.cmxs, but rather use some Makefile variables such
as foo$(DYNLIB), whose content is later set according to $(OPT)
Diffstat (limited to 'Makefile.build')
0 files changed, 0 insertions, 0 deletions