aboutsummaryrefslogtreecommitdiff
path: root/install.sh
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-04-18 14:16:08 +0000
committerGitHub2021-04-18 14:16:08 +0000
commitf67f789aa967fc4061861177cc2827ba9b2d2510 (patch)
treec8fd7a57f846b93c58289ba76325fd1ee094c086 /install.sh
parentd230b696a8b476e1c86f00a3ca5631ab6db83e40 (diff)
parent90871c4e9b2c2ea6983f4f37e33dd9c6fd2854a7 (diff)
Merge PR #14115: Change `Coqlib.lib_ref` to fail with `NameNotRegistered` instead of `UserError`
Reviewed-by: ejgallego Ack-by: herbelin
Diffstat (limited to 'install.sh')
0 files changed, 0 insertions, 0 deletions