misc: quote args in echoed command line

Currently if there are shell special characters in a
command-line argument, you can't copy and paste the
echoed command line onto a shell prompt because the
characters aren't quoted properly.  This patch fixes
that problem.

diff --git a/src/python/m5/main.py b/src/python/m5/main.py
index 29459cf647513668332b27d5fbb8215604ddf80d..700aae3d3bed40446e045b697295cf201ba8a8c3 100644 (file)
--- a/src/python/m5/main.py
+++ b/src/python/m5/main.py
@@ -293,9 +293,9 @@ def main(*args):
             datetime.datetime.now().strftime("%b %e %Y %X")
         print "gem5 executing on %s" % socket.gethostname()
 
-        print "command line:",
-        for argv in sys.argv:
-            print argv,
+        # in Python 3 pipes.quote() is moved to shlex.quote()
+        import pipes
+        print "command line:", " ".join(map(pipes.quote, sys.argv))
         print
 
     # check to make sure we can find the listed script