aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-24 14:18:03 +0000
committerGitHub2020-11-24 14:18:03 +0000
commit90cb2b0daf54cbd72c5ac8e1ffe2007c8901ddba (patch)
tree1b5149741dd0881050c9ecc3a8206f3062b6e3ac /engine
parentfa70203a836b0b4482a9d053af1af438cc0b4240 (diff)
parentf5ccc82ce8f2db919b288f3a853dbf238615de59 (diff)
Merge PR #13444: Fixes another instance of bug #7967 and #8076: restriction of universes in "Context"
Reviewed-by: SkySkimmer
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions