diff options
| author | Jason Gross | 2020-08-25 14:45:23 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-08-25 14:47:44 -0400 |
| commit | 3fab804cb9a07a8ccd936205e301413bfdfd37fb (patch) | |
| tree | 166f9f4bb01e4be28102d3c93a97fa84e8f463a4 /dev/header.ml | |
| parent | 51c0d56a5b0384e2f6bd980a1111547641c66b3e (diff) | |
Remove useless commit guessing logic
On GitLab, we don't need to base the job info on the PR number, since
it ought to be available from the git repo. Removing the logic will
make the bench infrastructure more uniform.
Diffstat (limited to 'dev/header.ml')
0 files changed, 0 insertions, 0 deletions