--verbose flag shows file names, not passed on to GF

2018-08-09 09:52:41 +02:00
parent e73d42379c
commit 60f19691eb
3 changed files with 14 additions and 17 deletions
--- a/Make.sh
+++ b/Make.sh
@@ -54,11 +54,6 @@ src="src"
 dist="dist"
 gfc="${gf} --batch --quiet"

-# Redirect stderr if not verbose
-if [ $verbose = false ]; then
-  exec 2> /dev/null
-fi
-
 # Make directories if not present
 mkdir -p "${dist}/prelude"
 mkdir -p "${dist}/present"