Remove trailing whitespace.

diff --git a/src/utils/pintos b/src/utils/pintos
index a86e8de282973d2a6f9f5d209b2e52a34618d045..ea4bdcc5da20dbb4c1d7956bedace31a8849f15d 100755 (executable)
--- a/src/utils/pintos
+++ b/src/utils/pintos
@@ -23,17 +23,17 @@ GetOptions ("sim=s" => sub { set_sim (@_) },
            "no-debug" => sub { set_debug ("no-debug") },
            "monitor" => sub { set_debug ("monitor") },
            "gdb" => sub { set_debug ("gdb") },
-           
+
            "run|get|put|make-disk" => \&cmd_option,
-           
+
            "m|memory=i" => \$mem,
            "j|jitter=i" => sub { set_jitter (@_) },
            "r|realtime" => sub { set_realtime () },
-           
+
            "v|no-vga" => sub { set_vga ('none'); },
            "s|no-serial" => sub { $serial_out = 0; },
            "t|terminal" => sub { set_vga ('terminal'); },
-           
+
            "h|help" => sub { usage (0); },
 
            "0|os-disk|disk-0|hda=s" => \$disks[0],
@@ -113,7 +113,7 @@ if ($cmd eq 'run') {
     # Create scratch disk from file.
     die "$hostfn: $!\n" if ! -e $hostfn;
     my ($size) = -s _;
-    if ($size) { 
+    if ($size) {
        copy_pad ($hostfn, "scratch.dsk", 512);
     } else {
        open (SCRATCH, ">scratch.dsk") or die "scratch.dsk: create: $!\n";