From: Ben Pfaff Date: Mon, 20 Jun 2005 21:53:43 +0000 (+0000) Subject: Allow decimal point in percentages. X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=1b18b7d238bdd54d416331436220e4517c4b35db;p=pintos-anon Allow decimal point in percentages. --- diff --git a/src/tests/make-grade b/src/tests/make-grade index f8c1443..e6c4b9c 100755 --- a/src/tests/make-grade +++ b/src/tests/make-grade @@ -25,7 +25,7 @@ open (GRADING, '<', $grading_file) || die "$grading_file: open: $!\n"; while () { s/#.*//; next if /^\s*$/; - my ($max_pct, $rubric_suffix) = /^\s*(\d+)%\t(.*)/ or die; + my ($max_pct, $rubric_suffix) = /^\s*(\d+(?:\.\d+)?)%\t(.*)/ or die; my ($dir) = $rubric_suffix =~ /^(.*)\//; my ($rubric_file) = "$src_dir/$rubric_suffix"; open (RUBRIC, '<', $rubric_file) or die "$rubric_file: open: $!\n";