devcontainer: add doc, user to match host machine, and scripts to build/start

2026-01-10 13:39:41 -08:00
parent 381d648be0
commit e0e6046afe
4 changed files with 98 additions and 1 deletions
--- a/ops/devcontainer/build.sh
+++ b/ops/devcontainer/build.sh
@@ -0,0 +1,9 @@
+#!/bin/sh
+
+SCRIPT_PATH=$(cd "$(dirname "$0")" && pwd)
+
+sudo docker build  \
+    --build-arg USERNAME="$(whoami)" \
+    --build-arg UID="$(id -u)" \
+    --build-arg GID="$(id -g)" \
+    -t gas "$SCRIPT_PATH"