Replace delete by destroy in comments dealing with states.
* src/tgba/succiter.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbaunion.hh, src/tgbaalgos/bfssteps.hh, src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/explscc.hh, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/replayrun.cc, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh: Update comments to say that we "destroy" a state instead of "deleting" it.
This commit is contained in:
parent
95cc50da51
commit
0c9c9fc639
13 changed files with 41 additions and 18 deletions
|
|
@ -198,7 +198,7 @@ namespace spot
|
|||
}
|
||||
|
||||
delete succ;
|
||||
// Do not delete CURR: it is a key in H.
|
||||
// Do not destroy CURR: it is a key in H.
|
||||
continue;
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue