diff --git a/src/plugins/e-acsl/scripts/testrun.sh b/src/plugins/e-acsl/scripts/testrun.sh
index ab14bb1b24a55a437732edfe490df57dff0a475a..ae5957ac2ff86cc6225e1a9ce08227639e719173 100755
--- a/src/plugins/e-acsl/scripts/testrun.sh
+++ b/src/plugins/e-acsl/scripts/testrun.sh
@@ -60,7 +60,9 @@ RUNS=1
 # Error reporting
 error() {
   echo "Error: $1" 1>&2
-  echo "See $2 for details" 1>&2
+  if [ -n "$DEBUG" ]; then
+    echo "See $2 for details" 1>&2
+  fi
   exit 1
 }