Dashboard: Revive generate_regtest_survey.py

This commit is contained in:
Ole Schütt 2022-03-02 23:31:01 +01:00 committed by Ole Schütt
parent 18911e0f42
commit fdd6874953
2 changed files with 92 additions and 96 deletions

View file

@ -31,6 +31,7 @@ run_test ./tools/docker/generate_dockerfiles.py --check
run_test mypy --strict ./tools/minimax_tools/minimax_to_fortran_source.py
run_test mypy --strict ./tools/dashboard/generate_dashboard.py
run_test mypy --strict ./tools/dashboard/generate_regtest_survey.py
run_test mypy --strict ./tools/regtesting/do_regtest.py
run_test mypy --strict ./tools/regtesting/optimize_test_dirs.py
run_test mypy --strict ./tools/precommit/check_file_properties.py