From 5f55abfa2327e26513637fc13586580d667b3ca6 Mon Sep 17 00:00:00 2001
From: Sears Russell <sears@cs.berkeley.edu>
Date: Mon, 12 Oct 2009 22:25:55 +0000
Subject: [PATCH] add support for #!/usr/bin/env timer.pl

---
 src/timing/timer.pl | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/src/timing/timer.pl b/src/timing/timer.pl
index ebf5600..55ba082 100755
--- a/src/timing/timer.pl
+++ b/src/timing/timer.pl
@@ -2,6 +2,7 @@
 
 use strict;
 
+my $infile;
 
 my $CI80 = 1;
 my $CI90 = 2;
@@ -138,6 +139,9 @@ while (@ARGV) {
 	print "tdist: $tdist\n";
 	shift @ARGV;
 	shift @ARGV;
+    } elsif (-f $ARGV[0] ) {
+	$infile = $ARGV[0];
+	shift @ARGV;
     }
 
     else {
@@ -148,6 +152,20 @@ while (@ARGV) {
 parse_t_distribution;
 
 
-while (my $cmd = <>) {
-    runbatch($cmd);
+if($infile) {
+  open IN, $infile;
+  while (my $cmd = <IN>) {
+    if($cmd !~ /^#/) {
+	print $cmd;
+        runbatch($cmd);
+    }
+  }
+  close IN;
+} else {
+  while (my $cmd = <>) {
+    if($cmd !~ /^#/) {
+	print $cmd;
+        runbatch($cmd);
+    }
+  }
 }