diff options
| author | Eric Engestrom <eric@engestrom.ch> | 2020-07-21 02:26:58 +0200 |
|---|---|---|
| committer | Marge Bot <eric+marge@anholt.net> | 2020-07-24 11:10:13 +0000 |
| commit | ccb91bc68c5b04d98d27a922a6a164928b789187 (patch) | |
| tree | 00bb28a29d127feb06e8e45dcac2a2c862b9c88a /bin | |
| parent | de5130fea05e9c441da64014d33d5d93254d7eca (diff) | |
bin/khronos-update: having a folder in include/ is not a requirement
Signed-off-by: Eric Engestrom <eric@engestrom.ch>
Part-of: <https://gitlab.freedesktop.org/mesa/mesa/-/merge_requests/6004>
Diffstat (limited to 'bin')
| -rwxr-xr-x | bin/khronos-update.py | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/bin/khronos-update.py b/bin/khronos-update.py index f95c8950419..68801d507e0 100755 --- a/bin/khronos-update.py +++ b/bin/khronos-update.py @@ -197,6 +197,7 @@ if __name__ == '__main__': source.sync() # Make sure all the API files are handled by this script - for file in pathlib.Path('include/' + group['inc_folder']).iterdir(): - if file not in [source.file for source in group['sources']]: - error('{} is unknown, please add it to SOURCES'.format(file)) + if 'inc_folder' in group: + for file in pathlib.Path('include/' + group['inc_folder']).iterdir(): + if file not in [source.file for source in group['sources']]: + error('{} is unknown, please add it to SOURCES'.format(file)) |