diff options
author | Rasmus Andersson <rasmus@notion.se> | 2020-05-18 18:47:33 +0300 |
---|---|---|
committer | Rasmus Andersson <rasmus@notion.se> | 2020-05-18 18:47:33 +0300 |
commit | 717605c5cd173ff84690c2daf51c1b54589278d9 (patch) | |
tree | 7b87170a96baf0381539248444f9caa09e91fe06 /misc/tools/dockermake | |
parent | 996c6f4f8137aa1a098f61471ec3a1ff6edc2cc6 (diff) | |
download | inter-717605c5cd173ff84690c2daf51c1b54589278d9.tar.xz |
tooling: Remove dockermake and fix a mkdir issue in init.sh. Closes #277
Diffstat (limited to 'misc/tools/dockermake')
-rwxr-xr-x | misc/tools/dockermake | 11 |
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 "$@" |