tracediff: Check for --debug-flags now instead of --trace-flags.
authorGabe Black <gblack@eecs.umich.edu>
Sun, 3 Jul 2011 05:52:26 +0000 (22:52 -0700)
committerGabe Black <gblack@eecs.umich.edu>
Sun, 3 Jul 2011 05:52:26 +0000 (22:52 -0700)
util/tracediff

index 5349c303d99713dd93d1fe5a28ac74024c9be8cb..5c77d9caff036d88e0cc5b19293aa653c7a16d3b 100755 (executable)
@@ -124,11 +124,11 @@ $sim2 = shift @cmd2;
 $args1 = join(' ', @cmd1);
 $args2 = join(' ', @cmd2);
 
-# Common mistake: if you don't set any traceflags this often isn't
+# Common mistake: if you don't set any debugflags this often isn't
 # doing what you want.
-if ($args1 !~ /--trace-flags/) {
+if ($args1 !~ /--debug-flags/) {
     print "****\n";
-    print "**** WARNING: no trace flags set... you may not be diffing much!\n";
+    print "**** WARNING: no debug flags set... you may not be diffing much!\n";
     print "****\n";
 }