From b9fa06564ced0621ea4fc6d537a6ce6d594e6256 Mon Sep 17 00:00:00 2001 From: Paul Cristian Sarbu Date: Thu, 17 Nov 2022 15:20:57 +0100 Subject: Bootstrap: Exclude other_tools folder from source files gathering --- bin/bootstrap.py | 2 ++ 1 file changed, 2 insertions(+) (limited to 'bin/bootstrap.py') diff --git a/bin/bootstrap.py b/bin/bootstrap.py index a8030e12..211570a2 100755 --- a/bin/bootstrap.py +++ b/bin/bootstrap.py @@ -261,6 +261,8 @@ def bootstrap(): dirs.remove('test') if 'execution_api' in dirs: dirs.remove('execution_api') + if 'other_tools' in dirs: + dirs.remove('other_tools') for f in files: if f.endswith(".cpp"): cpp_files.append(os.path.join(root, f)) -- cgit v1.2.3