Skip to content

Fix/tue decider error#17

Open
TWTDIG wants to merge 3 commits intomwernerds:masterfrom
TWTDIG:fix/tue_decider_error
Open

Fix/tue decider error#17
TWTDIG wants to merge 3 commits intomwernerds:masterfrom
TWTDIG:fix/tue_decider_error

Conversation

@TWTDIG
Copy link
Copy Markdown

@TWTDIG TWTDIG commented Nov 15, 2018

Proposed fix for TUE decider issue by checking for duplicates during (progressive) simplification.

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