aboutsummaryrefslogtreecommitdiff
path: root/ide/protocol/interface.ml
diff options
context:
space:
mode:
authorMaxime Dénès2018-12-04 10:33:47 +0100
committerMaxime Dénès2018-12-06 11:09:27 +0100
commit3e275d4bd1c3eb002b68c36ab116e5ab687d52f3 (patch)
tree6ea705714c862ab019aa312daf42d40ca50a4ace /ide/protocol/interface.ml
parenta2c8b7df8a0702ab716c0b97ad63d235b58b93a0 (diff)
Fix race condition triggered by fresh universe generation
Remote counters were trying to build universe levels (as opposed to simple integers), but did not have access to the right dirpath at construction time. We fix it by constructing the level only at use time, and we introduce some abstractions for qualified and unqualified level names.
Diffstat (limited to 'ide/protocol/interface.ml')
0 files changed, 0 insertions, 0 deletions