Skip to content

Optional duplicate skipping#74

Merged
fkirc merged 5 commits intomasterfrom
optional_duplicate_skipping
Dec 18, 2020
Merged

Optional duplicate skipping#74
fkirc merged 5 commits intomasterfrom
optional_duplicate_skipping

Conversation

@fkirc
Copy link
Copy Markdown
Owner

@fkirc fkirc commented Dec 18, 2020

A bugfix for #73.
The combination of "optional duplicate skipping" and "path skipping" did not work out as expected.

@fkirc fkirc merged commit 79840b1 into master Dec 18, 2020
@fkirc fkirc deleted the optional_duplicate_skipping branch December 18, 2020 15:51
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.

1 participant