X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pintos-anon;a=blobdiff_plain;f=src%2Futils%2Fpintos;h=fca610a15c83d6c4cdd1e80062d04b1812f5d1f8;hp=d7870351c0e966a9cf1263539aba2a9390bf55c2;hb=8349a4cbeec56e4b497d98064ce51aba80c1f258;hpb=3edcfedb8e62970f3293fa676b6691f8658c3c11

diff --git a/src/utils/pintos b/src/utils/pintos
index d787035..fca610a 100755
--- a/src/utils/pintos
+++ b/src/utils/pintos
@@ -259,7 +259,8 @@ sub prepare_scratch_disk {
 	  foreach @puts;
 
 	# Write end-of-archive marker.
-	print { $disks{SCRATCH}{HANDLE} } "\0" x 1024;
+	write_fully ($disks{SCRATCH}{HANDLE}, $disks{SCRATCH}{FILE_NAME},
+		     "\0" x 1024);
     }
 
     # Make sure the scratch disk is big enough to get big files.