tooling: Remove dockermake and fix a mkdir issue in init.sh. Closes #277

1 files changed, 11 insertions, 0 deletions

diff --git a/misc/tools/dockermake b/misc/tools/dockermake
new file mode 100755
index 000000000..3a6e21901
--- /dev/null
+++ b/misc/tools/dockermake
@@ -0,0 +1,11 @@
+#!/bin/bash -e
+#
+# Runs make in a prebuilt docker image.
+# All you need to have installed is docker for this to work.
+# This is an alternative to building locally.
+#
+cd "$(dirname "$0")"
+if [[ -d .git ]]; then
+  git rev-parse --short HEAD > githash.txt
+fi
+docker run --rm -it -v "$PWD:/host" rsms/inter-build:latest make -r -R "$@"