From fb828b3d279f4c1edbf04e53bde33a29b58ad6a3 Mon Sep 17 00:00:00 2001 From: Sergio Martins Date: Wed, 1 Jan 2025 23:31:47 +0000 Subject: [PATCH] ci: Move docker/ into .github Since this is the docker stuff for the GH runner. The development docker is in .devcontainer/ --- {docker => .github/docker}/Dockerfile | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename {docker => .github/docker}/Dockerfile (100%) diff --git a/docker/Dockerfile b/.github/docker/Dockerfile similarity index 100% rename from docker/Dockerfile rename to .github/docker/Dockerfile