diff options
| author | Ronan Pigott <ronan@rjp.ie> | 2022-11-16 15:50:34 -0700 |
|---|---|---|
| committer | Simon Ser <contact@emersion.fr> | 2022-11-26 10:29:59 +0100 |
| commit | 25f559dcdefa4781cd2a9da7d5bb92951adcb5eb (patch) | |
| tree | 0324f45b16899066845fd6aeaca461dd54527cf1 /.github | |
| parent | 52166bc1f530f477a6786707edf4b503e1a92cf5 (diff) | |
root: move the workspace matching code to its own file
This removes the pid_workspace bits from tree/root before it gets
too interesting.
No functional change.
(cherry picked from commit eb5021ef990fb29ff86544aea58d687ad62c757a)
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions