diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json deleted file mode 100644 index 1e54173..0000000 --- a/.devcontainer/devcontainer.json +++ /dev/null @@ -1,28 +0,0 @@ -// For format details, see https://aka.ms/devcontainer.json. For config options, see the -// README at: https://github.com/devcontainers/templates/tree/main/src/python -{ - "name": "Python 3", - // Or use a Dockerfile or Docker Compose file. More info: https://containers.dev/guide/dockerfile - "image": "mcr.microsoft.com/devcontainers/python:1-3.12-bullseye", - - // Features to add to the dev container. More info: https://containers.dev/features. - "features": { - "ghcr.io/devcontainers-contrib/features/actions-runner:1": {} - }, - - // Use 'forwardPorts' to make a list of ports inside the container available locally. - // "forwardPorts": [], - - // Use 'postCreateCommand' to run commands after the container is created. - // Clone the submodules, and install all the dependencies. - "postCreateCommand": { - "get_tinytex": "git submodule update --init", - "install_dependencies": "pip install .[dev,tests,docs]" - } - - // Configure tool-specific properties. - // "customizations": {}, - - // Uncomment to connect as root instead. More info: https://aka.ms/dev-containers-non-root. - // "remoteUser": "root" -}