diff options
author | John MacFarlane <jgm@berkeley.edu> | 2021-03-06 16:34:45 -0800 |
---|---|---|
committer | John MacFarlane <jgm@berkeley.edu> | 2021-03-06 16:34:45 -0800 |
commit | 271dd9e34445d09cdf12bb91de48bb0bfa7a1125 (patch) | |
tree | 389da82d1f29c7e07115fcb10b17ade6b4f12841 | |
parent | 1eb882fcdb6f1e8debde4a9805a69b815c574c64 (diff) | |
download | pandoc-271dd9e34445d09cdf12bb91de48bb0bfa7a1125.tar.gz |
make debpkg: send docker output to docker.log in the host.
Otherwise once the container is gone we can't figure out
what happened.
-rw-r--r-- | Makefile | 6 |
1 files changed, 4 insertions, 2 deletions
@@ -2,6 +2,7 @@ version?=$(shell grep '^[Vv]ersion:' pandoc.cabal | awk '{print $$2;}') pandoc=$(shell find dist -name pandoc -type f -exec ls -t {} \; | head -1) SOURCEFILES?=$(shell git ls-tree -r master --name-only | grep "\.hs$$") BRANCH?=master +ARCH=$(shell uname -m) DOCKERIMAGE=registry.gitlab.b-data.ch/ghc/ghc4pandoc:8.10.4 COMMIT=$(shell git rev-parse --short HEAD) TIMESTAMP=$(shell date "+%Y%m%d_%H%M") @@ -80,14 +81,15 @@ checkdocs: ! grep -q -n -e "\t" MANUAL.txt changelog.md debpkg: man/pandoc.1 - docker run -v `pwd`:/mnt \ + (docker run -v `pwd`:/mnt \ -v `pwd`/linux/artifacts:/artifacts \ -e REVISION=$(REVISION) \ -w /mnt \ --memory=0 \ + --rm \ $(DOCKERIMAGE) \ bash \ - /mnt/linux/make_artifacts.sh + /mnt/linux/make_artifacts.sh) 2>&1 > docker.log man/pandoc.1: MANUAL.txt man/pandoc.1.before man/pandoc.1.after pandoc $< -f markdown -t man -s \ |