aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/README-users.md
AgeCommit message (Expand)Author
2020-03-12[ci] [doc] Point to actual docker instructions.Emilio Jesus Gallego Arias
2020-01-31Clarify expectations for overlays in contributing guide and CI doc.Théo Zimmermann
2019-04-24[coq_makefile] Enforce warn_error for plugins.Emilio Jesus Gallego Arias
2018-11-24Apply suggestions from code review Théo Zimmermann
2018-11-24[ci] [doc] Note about `overlay-maintainers` team.Emilio Jesus Gallego Arias
2018-11-24[ci] [doc] Split user/developer README, add info about Nix/Docker CIEmilio Jesus Gallego Arias