aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.dev
Commit message (Expand)AuthorAge
* [camlpX] Enrico's changes to camlp4 removal.Gravatar Emilio Jesus Gallego Arias2017-04-07
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\
| * Missing .PHONY targets.Gravatar Pierre-Marie Pédrot2016-08-30
* | No more dev/printers.cmaGravatar Pierre Letouzey2016-07-26
* | Makefile.dev: fix a typo in the 'logic' ruleGravatar Pierre Letouzey2016-07-13
| * Makefile.dev: fix a typo in the 'logic' ruleGravatar Pierre Letouzey2016-07-13
|/
* Makefile.install: fix the install of plugin cmiGravatar Pierre Letouzey2016-06-24
* Makefile.build split in many smaller files : Makefile.{ide,checker,dev,install}Gravatar Pierre Letouzey2016-06-08