| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-12-10 | [ci] simplify overlay scripts | Enrico Tassi | |
| 2020-10-12 | Automatically merge overlays with most recent upstream version | Gaƫtan Gilbert | |
| This avoids the need to rebase the overlay when nothing has changed. | |||
| 2019-02-21 | remove meta trailing whitespace | Enrico Tassi | |
| 2018-11-22 | [dev] fix create_overlay wrt branch names containing / | Enrico Tassi | |
| 2018-11-17 | [devtools] Small script to setup overlays automatically | Emilio 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. | |||
