1 files changed, 1 insertions, 1 deletions
diff --git a/b b/b
index e505cdf5..88474475 100755
--- a/b
+++ b/b
@@ -1,5 +1,5 @@
 #!/bin/bash
-args="-O2 -fwarn-unused-imports -rtsopts"
+args="-O2 -fwarn-unused-imports -rtsopts -DRENDERFLUSH"
 root=${0%/*}
 cd "$root"

diff --git a/b b/b index e505cdf5..88474475 100755 --- a/b +++ b/b
@@ -1,5 +1,5 @@
1	#!/bin/bash	1	#!/bin/bash
2	args="-O2 -fwarn-unused-imports -rtsopts"	2	args="-O2 -fwarn-unused-imports -rtsopts -DRENDERFLUSH"
3		3
4	root=${0%/*}	4	root=${0%/*}
5	cd "$root"	5	cd "$root"