tree 40467f0befa2cf082f8531a13f1be8dad5a9df1f
parent ea8927a84a6011baa39a6be76d66d910a262d63d
author Julian Hyde <julianhyde@gmail.com> 1381258769 -0700
committer Julian Hyde <julianhyde@gmail.com> 1381258769 -0700

Make sure Enumerator.close() is always called.