diff options
| author | gumi <git@gumi.ca> | 2019-05-06 09:56:15 -0400 |
|---|---|---|
| committer | gumi <git@gumi.ca> | 2019-05-06 09:56:15 -0400 |
| commit | fa6a3682e85d5fbfc8aab6ad3abbc73c2eb15e45 (patch) | |
| tree | ba89e3dc41534b9ac26a18b99f3f24bd381ed01f | |
| parent | b0f6fb4b280b11ba96edbd1841e0c060363130a0 (diff) | |
| download | evol-tools-fa6a3682e85d5fbfc8aab6ad3abbc73c2eb15e45.tar.gz evol-tools-fa6a3682e85d5fbfc8aab6ad3abbc73c2eb15e45.tar.bz2 evol-tools-fa6a3682e85d5fbfc8aab6ad3abbc73c2eb15e45.tar.xz evol-tools-fa6a3682e85d5fbfc8aab6ad3abbc73c2eb15e45.zip | |
allow to use valgrind/gdb on the test server wrapper
| -rwxr-xr-x | herculeswrapper/map.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/herculeswrapper/map.sh b/herculeswrapper/map.sh index 055acd7..d0cd929 100755 --- a/herculeswrapper/map.sh +++ b/herculeswrapper/map.sh @@ -9,7 +9,7 @@ source ${dir}/include.sh create_pipe while [ 1 ] ; do - ./map-server + $DEBUG_MAP ./map-server export ret=$? case "${ret}" in 0) @@ -18,7 +18,7 @@ while [ 1 ] ; do ;; 1) echo "Returned 1. Probably error in server" - break + [ ! -z "$DEBUG_MAP" ] || break ;; 100) echo "Terminating server" |