aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/create_overlays.sh
AgeCommit message (Collapse)Author
2020-12-10[ci] simplify overlay scriptsEnrico Tassi
2020-10-12Automatically merge overlays with most recent upstream versionGaƫtan Gilbert
This avoids the need to rebase the overlay when nothing has changed.
2019-02-21remove meta trailing whitespaceEnrico Tassi
2018-11-22[dev] fix create_overlay wrt branch names containing /Enrico Tassi
2018-11-17[devtools] Small script to setup overlays automaticallyEmilio Jesus Gallego Arias
This is very preliminary but you should get the idea. The script tries to build contribs, then creates a branch and sets the remote properly as to submit a PR. Usage example: ``` ./dev/tools/create_overlays.sh ejgallego 9999 ltac2 elpi ``` This only works for contributions hosted in github for now.