Add configuration for GitHub Codespaces

This should allow using Julia in GitHub codespaces with Oscar.jl
oscar-system · Feb 13, 2021 · 5a5f2b0 · 5a5f2b0
1 parent d0908f5
commit 5a5f2b0
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
@@ -0,0 +1,10 @@
+// For format details, see https://aka.ms/devcontainer.json. For config options, see the README at:
+// https://github.com/microsoft/vscode-dev-containers/tree/v0.155.1/containers/julia
+// See https://github.com/julia-vscode/julia-devcontainer/blob/master/Dockerfile for image contents
+{
+	"name": "Julia (Community)",
+	"image": "ghcr.io/julia-vscode/julia-devcontainer",
+	"extensions": ["julialang.language-julia"],
+	"postCreateCommand": "/julia-devcontainer-scripts/postcreate.jl",
+	"remoteUser": "vscode"
+}