aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/user-overlays
AgeCommit message (Expand)Author
2017-12-08Merge PR #6158: Allows a level in the raw and glob printersMaxime Dénès
2017-11-27Adding overlay for ltac2.Hugo Herbelin
2017-11-25Overlay for stronger restrict_universe_context.Gaëtan Gilbert
2017-11-22[plugin] Remove LocalityFixme über hack.Emilio Jesus Gallego Arias
2017-06-16Each user overlay goes into its own file.Théo Zimmermann