aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib/Library.tex
diff options
context:
space:
mode:
authorThéo Zimmermann2020-04-03 09:25:17 +0200
committerThéo Zimmermann2020-04-03 14:40:46 +0200
commit57bb9a6ff1fa324c7bd918ab141678044504193d (patch)
treebcd1e3413857951c58307277343cb12a8e4f0917 /doc/stdlib/Library.tex
parente46e37ddabcb5ef2d58fd09dcc0a13a4b42f6b93 (diff)
Fix CoRN CI script.
Auto-generated files like the Makefile have recently been removed from the sources (cf. coq-community/corn#88). Calling ./configure.sh is now required.
Diffstat (limited to 'doc/stdlib/Library.tex')
0 files changed, 0 insertions, 0 deletions