# HG changeset patch
# User wenzelm
# Date 1262021831 -3600
# Node ID aecdcaaa8ff32529574ed417d9e169c2d7fe6f03
# Parent  c352f679dccac5be9f0c0b08ea3882d6c4cd74b5
pid without newline -- required for Scala version of system_out;

diff -r c352f679dcca -r aecdcaaa8ff3 lib/scripts/system.pl
--- a/lib/scripts/system.pl	Mon Dec 28 16:45:01 2009 +0100
+++ b/lib/scripts/system.pl	Mon Dec 28 18:37:11 2009 +0100
@@ -17,7 +17,7 @@
 }
 
 open (PID_FILE, ">", $pid_name) || die $!;
-print PID_FILE "$$\n";
+print PID_FILE "$$";
 close PID_FILE;