+
+ void _setFileLength(RandomAccessFile f, int length) throws IOException{
+ InputStream in = new FileInputStream(f.getFD());
+ OutputStream out = new FileOutputStream(f.getFD());
+
+ byte[] buf = new byte[1024];
+ for (int len; length > 0; length -= len) {
+ len = in.read(buf, 0, Math.min(length, buf.length));
+ if (len == -1) break;
+ out.write(buf, 0, len);
+ }
+ if (length == 0) return;
+
+ // fill the rest of the space with zeros
+ for (int i=0; i < buf.length; i++) buf[i] = 0;
+ while (length > 0) {
+ out.write(buf, 0, Math.min(length, buf.length));
+ length -= buf.length;
+ }
+ }
+