From d52d7c870959fe0c06ba1fe3be09cc8cbb112693 Mon Sep 17 00:00:00 2001 From: Michal Czyz Date: Tue, 22 Aug 2023 18:36:55 +0200 Subject: [PATCH] Create empty dev if old.dev does not exist --- .github/scripts/indexgen/generate.py | 37 ++++++++++++++-------------- 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/.github/scripts/indexgen/generate.py b/.github/scripts/indexgen/generate.py index 1b914757c82..0ba662c26f8 100755 --- a/.github/scripts/indexgen/generate.py +++ b/.github/scripts/indexgen/generate.py @@ -170,25 +170,26 @@ def main(): # Reports for development branches / pull requests branches = [] path = os.path.join(args.root, "dev") - for file in os.listdir(path): - if not os.path.isdir(os.path.join(path, file)): - continue - - branches.append(file) - - make_coverage_report_index( - file, - os.path.join(args.root, "dev", file), - os.path.join(args.output, "dev", file), - args.template - ) - make_verification_report_index( - file, - os.path.join(args.root, "dev", file), - os.path.join(args.output, "dev", file), - args.template - ) + if os.path.isdir(path): + for file in os.listdir(path): + if not os.path.isdir(os.path.join(path, file)): + continue + branches.append(file) + + make_coverage_report_index( + file, + os.path.join(args.root, "dev", file), + os.path.join(args.output, "dev", file), + args.template + ) + + make_verification_report_index( + file, + os.path.join(args.root, "dev", file), + os.path.join(args.output, "dev", file), + args.template + ) # Prepare the branch/pr index page make_dev_index(branches, args.output, args.template)