Skip to content

Re-introduce a fixed version of ExecuteDFS (Issue #487) #499

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
Draft
wants to merge 4 commits into
base: main
Choose a base branch
from
Draft

Re-introduce a fixed version of ExecuteDFS (Issue #487) #499

wants to merge 4 commits into from

Conversation

james-d-mitchell
Copy link
Member

This PR fixes some bugs introduced in #459

@wilfwilson

This comment has been minimized.

Sign in to view
@wilfwilson wilfwilson changed the title Dfs Fix problem with ExecuteDFS (issue #487) Sep 21, 2021
@wilfwilson wilfwilson mentioned this pull request Oct 27, 2021
Merged
@wilfwilson wilfwilson mentioned this pull request Oct 27, 2021
Draft
@wilfwilson wilfwilson changed the title Fix problem with ExecuteDFS (issue #487) Re-introduce a fixed version of ExecuteDFS (Issue #487) Oct 27, 2021
@wilfwilson
Copy link
Collaborator

This PR fixes the ExecuteDFS stuff, which is no longer in the master branch, but which is now contained in a separate branch on this repository called readd-new-dfs (see #504).

I have therefore rebased this PR on top of readd-new-dfs and pushed it to your branch. Therefore, merging this PR will re-introduce the ExecuteDFS stuff, but in a fixed state (fingers crossed!).

@wilfwilson wilfwilson mentioned this pull request Oct 27, 2021
Closed
@james-d-mitchell james-d-mitchell marked this pull request as draft January 5, 2022 13:14
@james-d-mitchell james-d-mitchell added the do not merge A label for PRs that should not be merged for whatever reason. label Jan 6, 2022
@saffronmciver saffronmciver mentioned this pull request Mar 4, 2025
Open
@digraphs digraphs deleted a comment from github-actions bot Sep 10, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
do not merge A label for PRs that should not be merged for whatever reason.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@james-d-mitchell @wilfwilson