add Hash.dumpkeys() that takes a preallocated array (may be of different element...
authoradam <adam@megacz.com>
Sat, 17 Mar 2007 08:51:20 +0000 (08:51 +0000)
committeradam <adam@megacz.com>
Sat, 17 Mar 2007 08:51:20 +0000 (08:51 +0000)
commitf716713c2bbd7eb4b0a1a9d3a0cff22644df864f
treed7824b6b3d2f7cff4f30b64f7d02bab9a3e30ff5
parentc293f2699600b1d1285edb2ab97e7ca240e58188
add Hash.dumpkeys() that takes a preallocated array (may be of different element type)

darcs-hash:20070317085120-5007d-33b898828841ecbc423e92ec31a109bfc654f583.gz
src/org/ibex/util/Hash.java