aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/build-system.txt
AgeCommit message (Expand)Author
2019-10-13Doc update with mlg extension - fix #10855mcaci
2019-05-22Update build-system.txtFourchaux
2019-05-21Fixing typos - Part 1JPR
2018-10-17[doc] [build] Remove ocamlbuild leftovers.Emilio Jesus Gallego Arias
2018-02-22Tweak developer documentation.Jim Fehrle
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
2016-06-21Makefile: compat5* moved in grammar/, less -I given to camlp4oPierre Letouzey
2016-06-01Yet another Makefile reform : a unique phase without nasty make tricksPierre Letouzey
2014-02-27Makefile: re-introduce 2 phases to avoid make strange -include'sPierre Letouzey
2012-09-20Remove broken makefile option NO_RECOMPILE_LIBletouzey
2010-03-04Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...letouzey
2008-09-06Use $(COQTOPEXE) to refer to bin/coqtop in Makefilesglondu
2008-06-05Fix typoslmamane
2008-02-13Implement KEEP_ML4_PREPROCESSED option in build systemlmamane
2008-02-13Implement NO_RECALC_DEPS option in build systemlmamane
2007-10-11Allow a few build system optimisations/corner-cuttinglmamane
2007-07-25Add glob.dump to Makefile the recommended way and document thelmamane
2007-07-16Reorganise cleaning targetslmamane
2007-07-13New bootstrapping, improved, Makefile systemcorbinea
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:30:26 +0000