| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
