diff options
author | John MacFarlane <jgm@berkeley.edu> | 2017-04-03 13:01:30 +0200 |
---|---|---|
committer | John MacFarlane <jgm@berkeley.edu> | 2017-04-03 13:01:30 +0200 |
commit | 12501f1000f592ff67cca98b6733f0bfa3115f9f (patch) | |
tree | 67ecdf3c50fb6ed3a6af2f20ae2d5250f21816bc /tools/make_entities_inc.py | |
parent | b75890e0fd7abb995d083b795c2cd45703b7cb22 (diff) |
Fixed code for freeing delimiter stack.
Note, however, that this may not be needed at all:
the old code would have gone into an infinite loop
if the delimiter stack were not already freed.
If we can prove that the delimiter stack is empty
at this point, we could remove this; on the other hand,
it may not hurt to keep it here defensively.
Closes #189.
Diffstat (limited to 'tools/make_entities_inc.py')
0 files changed, 0 insertions, 0 deletions