Skip to content

replace_symbolt can now replace tag type symbols#2845

Closed
kroening wants to merge 1 commit intodevelopfrom
replace-symbol-tags
Closed

replace_symbolt can now replace tag type symbols#2845
kroening wants to merge 1 commit intodevelopfrom
replace-symbol-tags

Conversation

@kroening
Copy link
Copy Markdown
Collaborator

Obvious interaction with #2723.

@tautschnig
Copy link
Copy Markdown
Collaborator

My understanding (as implemented in #2723) was that we don't need replacement for type symbols (or, for that matter, tags) at all?

@kroening
Copy link
Copy Markdown
Collaborator Author

Yes, my suspicion is that we simply won't need this eventually.

@tautschnig
Copy link
Copy Markdown
Collaborator

@kroening Can this be closed?

@tautschnig tautschnig assigned kroening and unassigned tautschnig Sep 3, 2018
@kroening kroening force-pushed the replace-symbol-tags branch from 6a12505 to 6dd3d3c Compare October 2, 2018 19:17
@TGWDB
Copy link
Copy Markdown
Contributor

TGWDB commented Jul 8, 2021

Closing as this as long neglected and also since the mentioned PR that may also solve the same issue (#2723) has been merged. Please reopen if you believe this is erroneous or something is missing.

@TGWDB TGWDB closed this Jul 8, 2021
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.

3 participants