From e7fa9c4c232c8411b1b118cd0f78d5d2aeec52e3 Mon Sep 17 00:00:00 2001 From: John MacFarlane <jgm@berkeley.edu> Date: Mon, 15 Aug 2022 22:47:14 -0700 Subject: [PATCH] make debpkg: get rid of docker.log. Let things come out on the CI output. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 4b65a5fff..df2d9cc44 100644 --- a/Makefile +++ b/Makefile @@ -91,7 +91,7 @@ debpkg: ## create linux package --rm \ $(DOCKERIMAGE) \ bash \ - /mnt/linux/make_artifacts.sh 2>&1 > docker.log + /mnt/linux/make_artifacts.sh man/pandoc.1: MANUAL.txt man/pandoc.1.before man/pandoc.1.after pandoc $< -f markdown -t man -s \