brush: vendor the source tree (un-ignore) to complete the local fork

The prior commit switched the recipe to `[source] path = "source"`, but .gitignore:77 still listed `local/recipes/shells/brush/source` (a leftover from when brush was a transient upstream git fetch), so the vendored tree was not tracked — a fresh clone would have no brush source and the build would fail. Drop that ignore line and commit the vendored working tree (reubeno/brush @ 897b373e, with the Redox port patches pre-applied). brush is now a durable local fork like the other path=source recipes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-07-26 23:34:31 +09:00
parent 0383dcbca3
commit 25fb843c40
675 changed files with 97606 additions and 1 deletions
@@ -0,0 +1,72 @@
+name: "Devcontainer"
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    paths:
+      - ".devcontainer/**"
+
+permissions: {}
+
+# Only allow one run of the workflow per branch / PR at a time.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    name: "Build devcontainer"
+    runs-on: ubuntu-24.04
+    permissions:
+      contents: read
+      packages: read
+    steps:
+      - name: Checkout sources
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        with:
+          persist-credentials: false
+
+      - name: Login to GitHub Container Registry
+        uses: docker/login-action@af1e73f918a031802d376d3c8bbc3fe56130a9b0 # v4.4.0
+        with:
+          registry: ghcr.io
+          username: ${{ github.repository_owner }}
+          password: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Pre-build dev container image
+        uses: devcontainers/ci@513af61f4de4f75d37e4438f184ba4358f0fc1ca # v0.3.1900000450
+        with:
+          imageName: ghcr.io/reubeno/brush/devcontainer
+          imageTag: latest
+          cacheFrom: ghcr.io/reubeno/brush/devcontainer
+          push: never
+
+  build_and_publish:
+    name: "Build and publish devcontainer"
+    runs-on: ubuntu-24.04
+    permissions:
+      contents: read
+      packages: write
+    steps:
+      - name: Checkout sources
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        with:
+          persist-credentials: false
+
+      - name: Login to GitHub Container Registry
+        uses: docker/login-action@af1e73f918a031802d376d3c8bbc3fe56130a9b0 # v4.4.0
+        with:
+          registry: ghcr.io
+          username: ${{ github.repository_owner }}
+          password: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Pre-build dev container image
+        uses: devcontainers/ci@513af61f4de4f75d37e4438f184ba4358f0fc1ca # v0.3.1900000450
+        with:
+          imageName: ghcr.io/reubeno/brush/devcontainer
+          imageTag: latest
+          cacheFrom: ghcr.io/reubeno/brush/devcontainer
+          push: filter
+          refFilterForPush: refs/heads/main
+          eventFilterForPush: push