Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Closed
tkw1536 opened this issue Oct 19, 2020 · 5 comments
Closed

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

tkw1536 opened this issue Oct 19, 2020 · 5 comments
Assignees
@florian-rabe
Labels
build system enhancement

Comments

@tkw1536
Copy link
Contributor

tkw1536 commented Oct 19, 2020

/cc @lambdaTotoro @florian-rabe
@ComFreek
Copy link
Member

5c83fc9 should have fixed it, no?

@ComFreek
Copy link
Member

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

@ComFreek ComFreek reopened this Oct 20, 2020
@lambdaTotoro
Copy link
Contributor

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
Copy link
Member

fixed

@ComFreek
Copy link
Member

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@florian-rabe florian-rabe

Labels
build system enhancement
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@lambdaTotoro @ComFreek @tkw1536 @florian-rabe