diff options
| author | mrb0nk500 <b0nk@b0nk.xyz> | 2022-07-13 16:08:59 -0300 |
|---|---|---|
| committer | mrb0nk500 <b0nk@b0nk.xyz> | 2022-07-13 16:41:50 -0300 |
| commit | b71a05e0bacff4f03fe75fba22197c3100d58c09 (patch) | |
| tree | 24a4398d58282d05b5d31dbac697da2ff322652f /.gitignore | |
| parent | b93ca4a3a70cad569e5ab8056923f90043b4b0e9 (diff) | |
git: Use an index instead of an id for creating PR directories
PR's will now be identified by index, rather than by id.
If no index is found, then it falls back to using the PR title as the
directory name.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions