From 3b39301d34d7a000325a42bbcfe880b53ac26154 Mon Sep 17 00:00:00 2001
From: klaar36 <klas.arvidsson@liu.se>
Date: Fri, 19 May 2017 15:05:06 +0200
Subject: imported misc scripts

---
 src/utils/debugpintos | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100755 src/utils/debugpintos

(limited to 'src/utils/debugpintos')

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
-- 
cgit v1.2.1