Allow PINTOSSIM environment variable to select default simulator.

diff --git a/src/utils/pintos b/src/utils/pintos
index 0c1f34d54aab6c79d1a7f6ec7cb81e0380c0545d..fe7d9544583b13960e4127b048e2d1f2f846d834 100755 (executable)
--- a/src/utils/pintos
+++ b/src/utils/pintos
@@ -8,7 +8,7 @@ use Getopt::Long qw(:config bundling);
 
 # Command-line options.
 our ($start_time) = time ();
-our ($sim);                    # Simulator: bochs, qemu, or gsx.
+our ($sim) = $ENV{PINTOSSIM};  # Simulator: bochs, qemu, or gsx.
 our ($debug) = "none";         # Debugger: none, monitor, or gdb.
 our ($mem) = 4;                        # Physical RAM in MB.
 our ($serial_out) = 1;         # Send output to serial port?
@@ -130,6 +130,8 @@ Disk options: (name an existing FILE or specify SIZE in MB for a temp disk)
   --swap-disk=FILE|SIZE    Set swap disk file (default: swap.dsk)
 Other options:
   -h, --help               Display this help message.
+Environment variables:
+  PINTOSSIM                Select default simulator.
 EOF
     exit $exitcode;
 }