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.

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

Rename edit-annotated because of clash with other QC check #1137

Merged
merged 1 commit into from
Aug 5, 2023

Conversation

matentzn
Copy link
Contributor

@matentzn matentzn commented Aug 5, 2023

  • docs/ have been added/updated (No need)
  • tests have been added/updated (the nature of this PR)
  • mvn verify says all tests pass
  • mvn site says all JavaDocs correct

In my attempts to migrate to the latest OWLAPI (#1135), I encountered a problem I could not understand which @gouttegd solved for me. Basically, the problem is that the test suite is slightly overlapping:

robot merge --input edit.owl --input edit2.owl --output results/merged2.owl
robot merge --inputs "edit*.owl" --output results/merged2.owl

Applying this PR, the test now passes, because the file then no longer matches the edit*.owl pattern in the second command that produces merged2.owl above, so it is no longer merged and therefore the resulting merged2.owl is identical to what the test expects.

Thank you @gouttegd for this uncovering this, it really made me puzzle!

What is, however, a bit unclear: why did this error only show up now?

Something for future generations to puzzle about.

@matentzn
Copy link
Contributor Author

matentzn commented Aug 5, 2023

EDIT: This works, and fixes, indeed #1135. @gouttegd in James absence, can you give me the thumbs up on this PR, so I can merge it?

@gouttegd
Copy link
Contributor

gouttegd commented Aug 5, 2023

If you mean formal approval, no I can’t: I am merely a contributor here, I don’t have commit privileges on this repo.

If you want an informal thumbs up, sure: I tested myself, it works. 👍

@matentzn
Copy link
Contributor Author

matentzn commented Aug 5, 2023

@gouttegd thank you, that is all I needed.

@matentzn matentzn merged commit 67a7b6c into master Aug 5, 2023
3 checks passed
@matentzn matentzn deleted the rename-edit-annotated branch August 5, 2023 13:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants