From 3fc637e2e94cae6f0cd00323775a691d2397300c Mon Sep 17 00:00:00 2001 From: Julian Oes Date: Fri, 12 Jul 2019 11:16:53 +0200 Subject: [PATCH] tools: choose correct dockerhub repo This was incorrectly set after the rename. --- tools/run-docker.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/run-docker.sh b/tools/run-docker.sh index d75aa43d9e..e907144585 100755 --- a/tools/run-docker.sh +++ b/tools/run-docker.sh @@ -1,3 +1,3 @@ #!/usr/bin/env sh -docker run -it --rm -v $(pwd):/home/user/MAVSDK:z -e LOCAL_USER_ID=`id -u` mavlink/mavsdk-ubuntu-18.04-px4-sitl "$@" +docker run -it --rm -v $(pwd):/home/user/MAVSDK:z -e LOCAL_USER_ID=`id -u` mavsdk/mavsdk-ubuntu-18.04-px4-sitl "$@"