diff options
| author | klaar36 <klas.arvidsson@liu.se> | 2017-05-19 15:05:06 +0200 |
|---|---|---|
| committer | klaar36 <klas.arvidsson@liu.se> | 2017-05-19 15:05:06 +0200 |
| commit | 3b39301d34d7a000325a42bbcfe880b53ac26154 (patch) | |
| tree | 9f5a239bf47da78358645c2ad1136972121cece7 /src/utils/debugpintos | |
| parent | 6fea0f8ce4ba0d08a414a1650c829afbef285f70 (diff) | |
| download | pintos-rs-3b39301d34d7a000325a42bbcfe880b53ac26154.tar.gz | |
imported misc scripts
Diffstat (limited to 'src/utils/debugpintos')
| -rwxr-xr-x | src/utils/debugpintos | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/utils/debugpintos b/src/utils/debugpintos new file mode 100755 index 0000000..8dfdc77 --- /dev/null +++ b/src/utils/debugpintos @@ -0,0 +1,7 @@ +#!/bin/bash + +if command -v mapsocket >/dev/null 2>&1; then + exec mapsocket -m 1234 dynamic spintos --gdb "$@" +else + exec pintos --gdb "$@" +fi |