diff options
Diffstat (limited to 'misc')
-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 "$@" |