diff options
| author | jvoisin | 2018-07-19 13:48:35 +0200 |
|---|---|---|
| committer | jvoisin | 2018-07-19 13:48:35 +0200 |
| commit | 606bef01543225e56378904b94bd41f41645f4be (patch) | |
| tree | cef79ddeade62e6c3e753354b8eb891230163e1f /src | |
| parent | 2a5accbb7c12b2d4a16359914c18ccf856251f53 (diff) | |
Document that you need to `git push` after the release :p
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions