Skip to content

merge_irept should not destroy comments (but it may ignore differences) - #32

Merged
kroening merged 1 commit into
diffblue:masterfrom
tautschnig:merge_irept-loses-comments
Apr 2, 2016
Merged

merge_irept should not destroy comments (but it may ignore differences)#32
kroening merged 1 commit into
diffblue:masterfrom
tautschnig:merge_irept-loses-comments

Conversation

@tautschnig

Copy link
Copy Markdown
Collaborator

We otherwise lose, e.g., ID_C_SSA_symbol

@kroening
kroening merged commit 7c271af into diffblue:master Apr 2, 2016
@tautschnig
tautschnig deleted the merge_irept-loses-comments branch June 20, 2016 10:01
smowton added a commit to smowton/cbmc that referenced this pull request May 9, 2018
…e-files

Added more IDE files to .gitignore
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Sep 9, 2026
…iffblue#31 latent bug

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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