| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-01-31 | [makefile] Ignore _build_boot directory | Emilio Jesus Gallego Arias | |
| PR #11267 reverted commit d21e17ac99dfb2008f2e2bfdb373413490d1ffc7 (of PR #10695) by error, this reinstates it. | |||
| 2019-12-16 | FIND_SKIP_DIRS (make): ignore all dot directories | Gaëtan Gilbert | |
| Fix #11266 | |||
| 2019-12-16 | [make] Add _build_boot to find_skip_dirs | Emilio Jesus Gallego Arias | |
| 2019-12-13 | [make] Rename Makefile to Makefile.make | Emilio Jesus Gallego Arias | |
| Picked from #8729. This should help preserve the history better when we split. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/Makefile.make