Merge branch 'dev-improvements' of https://github.com/guzman-raphael/datajoint-python into dev-improvements

Author: guzman-raphael

docs/src/develop.md

@@ -8,8 +8,8 @@ Here are some options that provide a great developer experience:
 
 - **Cloud-based IDE**: (*recommended*)
   - Launch using [GitHub Codespaces](https://github.com/features/codespaces) using the option `Create codespace on master` in the codebase repository on your fork.
-  - Build time for a 2-Core codespace is **~5m**. This is done infrequently and cached for convenience.
-  - Start time for a 2-Core codespace is **~1m**. This will pull the built codespace from cache when you need it.
+  - Build time for a 2-Core codespace is **~6m**. This is done infrequently and cached for convenience.
+  - Start time for a 2-Core codespace is **~2m**. This will pull the built codespace from cache when you need it.
   - *Tip*: GitHub auto names the codespace but you can rename the codespace so that it is easier to identify later.
 - **Local IDE**:
   - Ensure you have [Git](https://git-scm.com/book/en/v2/Getting-Started-Installing-Git)