From bf6e66ce3110678c4baeeaef00135ab0ca2f8e66 Mon Sep 17 00:00:00 2001
From: clubby789 <jamie@hill-daniel.co.uk>
Date: Sun, 22 Dec 2024 22:23:54 +0000
Subject: [PATCH] Document the `--dev` flag for `src/ci/docker/run.sh`

---
 src/ci/docker/README.md | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/ci/docker/README.md b/src/ci/docker/README.md
index 876787c30e537..90d1ef2b0ecb4 100644
--- a/src/ci/docker/README.md
+++ b/src/ci/docker/README.md
@@ -26,6 +26,14 @@ DEPLOY=1 ./src/ci/docker/run.sh x86_64-gnu
 while locally, to the `obj/$image_name` directory. This is primarily to prevent
 strange linker errors when using multiple Docker images.
 
+## Local Development
+
+To get an interactive shell in the Docker image, pass the `--dev` flag, e.g.:
+
+```
+./src/ci/docker/run.sh --dev x86_64-gnu
+```
+
 ## Filesystem layout
 
 - Each host architecture has its own `host-{arch}` directory, and those