diff options
| -rw-r--r-- | THANKS | 1 | ||||
| -rwxr-xr-x | examples/test | 9 |
2 files changed, 7 insertions, 3 deletions
@@ -82,6 +82,7 @@ Gavin Smith gavinsmith0123@gmail.com Georg Sauthoff gsauthof@TechFak.Uni-Bielefeld.DE George Neuner gneuner2@comcast.net Gilles Espinasse g.esp@free.fr +Giorgos Pap giorgos551pap@gmail.com Goran Uddeborg goeran@uddeborg.se Guido Trentalancia trentalg@aston.ac.uk H. Merijn Brand h.m.brand@hccnet.nl diff --git a/examples/test b/examples/test index 45a5d454..738dcae4 100755 --- a/examples/test +++ b/examples/test @@ -137,10 +137,13 @@ run () else cat out_eff fi + # Ignore informational messages from the JVM. if ! $noerr; then - sed -e 's/^/err: /g' \ - -e 's/Reducing stack by rule .* (line .*):/Reducing stack by rule XX (line XXX):/g' \ - err_eff + sed \ + -e '/^Picked up _JAVA_OPTIONS: /d' \ + -e 's/Reducing stack by rule .* (line .*):/Reducing stack by rule XX (line XXX):/g' \ + -e 's/^/err: /g' \ + err_eff fi } >eff |