diff options
| -rwxr-xr-x | tools/profile (renamed from tools/profile_requires) | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/tools/profile_requires b/tools/profile index 927467bc4e..927467bc4e 100755 --- a/tools/profile_requires +++ b/tools/profile |