Skip to content

Commit

Permalink
Merge pull request #109 from antmicro/mczyz/dashboard-files-hotfix
Browse files Browse the repository at this point in the history
Create empty dev if old.dev does not exist
  • Loading branch information
tmichalak authored Aug 25, 2023
2 parents cdccf7a + d52d7c8 commit ad37519
Showing 1 changed file with 19 additions and 18 deletions.
37 changes: 19 additions & 18 deletions .github/scripts/indexgen/generate.py
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit ad37519

Please sign in to comment.