aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc/build-system.txt
Commit message (Expand)AuthorAge
* Tweak developer documentation.Gravatar Jim Fehrle2018-02-22
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
* Makefile: compat5* moved in grammar/, less -I given to camlp4oGravatar Pierre Letouzey2016-06-21
* Yet another Makefile reform : a unique phase without nasty make tricksGravatar Pierre Letouzey2016-06-01
* Makefile: re-introduce 2 phases to avoid make strange -include'sGravatar Pierre Letouzey2014-02-27
* Remove broken makefile option NO_RECOMPILE_LIBGravatar letouzey2012-09-20
* Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...Gravatar letouzey2010-03-04
* Use $(COQTOPEXE) to refer to bin/coqtop in MakefilesGravatar glondu2008-09-06
* Fix typosGravatar lmamane2008-06-05
* Implement KEEP_ML4_PREPROCESSED option in build systemGravatar lmamane2008-02-13
* Implement NO_RECALC_DEPS option in build systemGravatar lmamane2008-02-13
* Allow a few build system optimisations/corner-cuttingGravatar lmamane2007-10-11
* Add glob.dump to Makefile the recommended way and document theGravatar lmamane2007-07-25
* Reorganise cleaning targetsGravatar lmamane2007-07-16
* New bootstrapping, improved, Makefile systemGravatar corbinea2007-07-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 13:09:16 +0000