Skip to content

Improve the build script, re-enable Search commands #69

Improve the build script, re-enable Search commands

Improve the build script, re-enable Search commands #69

Triggered via pull request August 28, 2024 19:08
Status Success
Total duration 3m 50s
Artifacts

build-schools.yml

on: pull_request
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

10 warnings
Build Schools on Linux (Coq latest)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
Build Schools on Linux (Coq latest): 2017-12-Birmingham/Part2_Fundamentals_Coq/fundamentals_lecture.v#L299
Not considering unicode character "̂" of unknown lexical status as
Build Schools on Linux (Coq latest): 2017-12-Birmingham/Part2_Fundamentals_Coq/fundamentals_lecture.v#L309
Not considering unicode character "̂" of unknown lexical status as
Build Schools on Linux (Coq latest)
Declaring arbitrary terms as hints is fragile; it is recommended to
Build Schools on Linux (Coq latest)
Declaring arbitrary terms as hints is fragile; it is recommended to
Build Schools on Linux (Coq latest): 2017-12-Birmingham/Part5_Set_Level_Mathematics/set_level_mathematics_exercises.v#L217
Interpreting this declaration as if a global declaration prefixed by