Add docker to the devcontainer

2022-06-19 00:58:50 +00:00
parent 1f8d4423a6
commit 7bb4386b65
5 changed files with 62 additions and 30 deletions
@@ -0,0 +1,18 @@
+#!/bin/bash
+
+set -euo pipefail
+
+readonly wanted_line_key="LOCAL_WORKSPACE_FOLDER"
+readonly wanted_line="${wanted_line_key}='${PWD}'"
+readonly file=".env"
+
+echo "Writing ${wanted_line} to ${file}" >&2
+if grep --quiet "^${wanted_line_key}=" "${file}"; then
+    sed --in-place "s,^${wanted_line_key}=.*,${wanted_line}," "${file}"
+else
+    echo "LOCAL_WORKSPACE_FOLDER='${PWD}'" >"${file}"
+fi
+
+set -x
+
+git submodule update --init