aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/CoqMakefile.in
Commit message (Collapse)AuthorAge
...
* | Quote $(OCAMLFIND) in CoqMakefile.in for WindowsGravatar Jason Gross2017-06-30
| | | | | | This, I hope, will fix [bug #5620](https://coq.inria.fr/bugs/show_bug.cgi?id=5620)
| * Better support for make TIMED=1 on WindowsGravatar Jason Gross2017-06-30
|/ | | | This fixes [bug #5619](https://coq.inria.fr/bugs/show_bug.cgi?id=5619)
* Move TIMER to right in front of COQCGravatar Jason Gross2017-06-15
| | | | | Save the COQC variable for the actual path to coqc, as per https://github.com/coq/coq/pull/742#pullrequestreview-44072778
* Fix `make TIMED=1` garbageGravatar Jason Gross2017-06-15
| | | It should not emit ` (user: 0.00 mem: 2852 ko)` multiple times
* Strip trailing whitespaceGravatar Jason Gross2017-06-15
|
* Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\
* \ Merge PR#698: Trunk miscGravatar Maxime Dénès2017-06-07
|\ \
* | | Fix coq_makefile uninstall target under OSX.Gravatar Maxime Dénès2017-06-01
| | |
| * | removing duplicate line from "tools/CoqMakefile.in"Gravatar Matej Košík2017-05-31
|/ /
| * coq_makefile : do not build bytecode versions of plugins by defaultGravatar Pierre Letouzey2017-05-30
|/ | | | | | | | | | | | | | | | | | 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)
* coq_makefile: build .cma for each .mlpackGravatar Enrico Tassi2017-05-27
| | | | | | | | It used to generate only .cmo (the packed one). While this works if the plugin has no external dependencies, it does not if it does. The bug affected only bytecode builds
* coq_makefile: use -include rather than includeGravatar Enrico Tassi2017-05-24
| | | | | This fixes bedrock and eliminates warnings. Thanks Jason Gross for debugging this!
* add the only targetGravatar Enrico Tassi2017-05-23
| | | | | | | | This makes the following work correctly: make only TGTS="foo bar" -j2 note that make foo bar -j2 is not doing what you think
* coq_makefile: avoid spurious ./ in generated .conf fileGravatar Enrico Tassi2017-05-23
|
* Restore 8.5, 8.6 compatibility of STDTIME, TIMECMDGravatar Jason Gross2017-05-23
|
* Make install a single colon target for retro compatibilityGravatar Enrico Tassi2017-05-23
|
* enters coq_makefile2Gravatar Enrico Tassi2017-05-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 19:19:19 +0000