jenkins-build: point to new dir named after the script

This changes out the arbitrary names used before.

diff --git a/jenkins-build b/jenkins-build
index c9dc3b81d5cc9140d447b6febc66779ea8405951..6ddc3edc36ad3a2255075df8aa279c219e523db0 100755 (executable)
--- a/jenkins-build
+++ b/jenkins-build
@@ -43,7 +43,7 @@ hostname || true
 
 # point to the Vagrant/VirtualBox configs created by reproducible_setup_fdroid_build_environment.sh
 # these variables are actually set in fdroidserver/jenkins-build-makebuildserver
-export SETUP_WORKSPACE=$(dirname $WORKSPACE)/fdroid/fdroidserver
+export SETUP_WORKSPACE=$(dirname $WORKSPACE)/reproducible_setup_fdroid_build_environment/fdroidserver
 export XDG_CONFIG_HOME=$SETUP_WORKSPACE
 export VBOX_USER_HOME=$SETUP_WORKSPACE/VirtualBox
 export VAGRANT_HOME=$SETUP_WORKSPACE/vagrant.d