aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.ide
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-29 12:12:53 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-29 13:17:19 +0200
commitdd134de0b068c70adb80c94921673086f0002c30 (patch)
tree9a482d44a6c031b14b1f2929da337e23828a3885 /Makefile.ide
parentff820359e7adb4a414f4796e342f43b5264580a5 (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.ide')
0 files changed, 0 insertions, 0 deletions