tree bf42ca12d593089cb894d8169a0bf73dde836cff
parent 056b41ff98fcac22d5272ee451a179e09f163da1
author Julian Hyde <julianhyde@gmail.com> 1371427231 -0700
committer Julian Hyde <julianhyde@gmail.com> 1371427231 -0700

Make Enumerator extend java.io.Closeable rather than AutoCloseable. The latter does not exist until JDK 1.7.