aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/build-system.dev.txt
AgeCommit message (Expand)Author
2019-05-23Fixing typos - Part 2JPR
2019-05-21Fixing typos - Part 1JPR
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
2017-07-05Makefile: fails if some .vo or .cm* file has no sourcePierre 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
2010-03-04Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...letouzey
2009-02-11Document how FIND_VCS_CLAUSE has to be usedlmamane
2007-07-16A cleaner solution to "make deletes .ml4.d files -> infinite loop" problemlmamane
2007-07-13New bootstrapping, improved, Makefile systemcorbinea