Document dev off better

Refs #848
sebst · Nov 10, 2023 · ac59662 · ac59662
1 parent 90e5b3c
commit ac59662
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/docs/dev.md b/docs/dev.md
@@ -181,5 +181,12 @@ Generally programmer editors should see tools if the environments are
 activated. If no, [let us know] and we’ll fix it.
 
 
+## Deactivating `dev`
+
+```sh
+$ dev off
+```
+
+
 
 [let us know]: https://github.com/pkgxdev/pkgx/issues/new