diff options
| author | Théo Zimmermann | 2017-11-28 15:05:52 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2017-11-29 15:46:17 +0100 |
| commit | bc1fb4be47578b4da554aef69150acd77e82aba1 (patch) | |
| tree | b404488198794cf3c445236554865b61e780a2ae /dev/base_include | |
| parent | b23df225c7df7883af6ecfa921986cfb6fd3cd7c (diff) | |
Fix PR merge script.
Was still relying on the existence of user-configured /pr/.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions