From: Ben Pfaff <blp@cs.stanford.edu>
Date: Wed, 5 Apr 2006 20:30:48 +0000 (+0000)
Subject: Allow PINTOSSIM environment variable to select default simulator.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pintos-anon;a=commitdiff_plain;h=c2417ce1b555ee6df2064795271498e58148877e

Allow PINTOSSIM environment variable to select default simulator.
---

diff --git a/src/utils/pintos b/src/utils/pintos
index 0c1f34d..fe7d954 100755
--- 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;
 }