diff options
| author | Paweł Redman <pawel.redman@gmail.com> | 2017-12-26 20:30:11 +0000 |
|---|---|---|
| committer | Paweł Redman <pawel.redman@gmail.com> | 2017-12-26 20:30:11 +0000 |
| commit | d00b66f0ad70a293b5ee5e612d130d1269cfbd6c (patch) | |
| tree | b3dce55ee7a08a84c6b11248a5e7d5dff11e41ff | |
| parent | 4271b89490e64d1bf775b8be62b7c9efbb4d0fb7 (diff) | |
Add an option to disable the GDB wrapper.
| -rwxr-xr-x | run-instance.sh | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/run-instance.sh b/run-instance.sh index 2776ba0..f155648 100755 --- a/run-instance.sh +++ b/run-instance.sh @@ -56,6 +56,11 @@ true ${TREMDED_PREFIX:="$PREFIX/bin/tremded@"} # Debugging true ${DEBUG:=1} +true ${NO_DEBUGGER:=0} + +if [ "$NO_DEBUGGER" -ne 0 ]; then + GDB_WRAPPER="exec" +fi ################### # The entry point # |