search

UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 22 forks source link

Raise an error when two archives with the same id are opened #549

Closed tkw1536 closed 3 years ago

tkw1536 commented 3 years ago

/cc @lambdaTotoro @florian-rabe

ComFreek commented 3 years ago

https://github.com/UniFormal/MMT/commit/5c83fc9b5757eaf9a186857cade116041914f29b should have fixed it, no?

ComFreek commented 3 years ago

Oh, actually not. That commit was to devel-names. (Until someone git cherrypicks this commit to devel, I'll reopen.)

lambdaTotoro commented 3 years ago

Yes, see the comment I left on the commit. It also prints the root of the new archive, while the error message indicates that it would be the old one.

florian-rabe commented 3 years ago

fixed

ComFreek commented 3 years ago

The fix was again on devel-names. I git cherry-picked the two commits related to this issue to devel now.