diff -r 1335bbfb066f -r 1868db0d1515 contrib/dockerdeb
--- a/contrib/dockerdeb	Sat May 12 13:17:01 2018 -0700
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-#!/bin/bash -eu
-
-. $(dirname $0)/dockerlib.sh
-. $(dirname $0)/packagelib.sh
-
-BUILDDIR=$(dirname $0)
-export ROOTDIR=$(cd $BUILDDIR/.. > /dev/null; pwd)
-
-checkdocker
-
-DISTID="$1"
-CODENAME="$2"
-PLATFORM="$1-$2"
-shift; shift # extra params are passed to build process
-
-OUTPUTDIR=${OUTPUTDIR:=$ROOTDIR/packages/$PLATFORM}
-
-initcontainer $PLATFORM
-
-# debuild only appears to be able to save built debs etc to .., so we
-# have to share the .. of the current directory with the docker
-# container and hope it's writable. Whee.
-dn=$(basename $PWD)
-
-if [ $(uname) = "Darwin" ] ; then
-    $DOCKER run -u $DBUILDUSER --rm -v $PWD/..:/mnt $CONTAINER \
-            sh -c "cd /mnt/$dn && make clean && make local"
-fi
-$DOCKER run -u $DBUILDUSER --rm -v $PWD/..:/mnt $CONTAINER \
-  sh -c "cd /mnt/$dn && DEB_BUILD_OPTIONS='${DEB_BUILD_OPTIONS:=}' contrib/builddeb --build --distid $DISTID --codename $CODENAME $@"
-contrib/builddeb --cleanup --distid $DISTID --codename $CODENAME
-if [ $(uname) = "Darwin" ] ; then
-    $DOCKER run -u $DBUILDUSER --rm -v $PWD/..:/mnt $CONTAINER \
-            sh -c "cd /mnt/$dn && make clean"
-fi