Move dev/ docs to development/ (#10453)

CONTRIBUTING.md

@@ -392,7 +392,7 @@ By now, you know the drill!
 # Notes for maintainers on merging PRs etc
 
 There are some notes for those with commit access to the project on how we
-manage git [here](docs/dev/git.md).
+manage git [here](docs/development/git.md).
 
 # Conclusion
 

changelog.d/10453.doc

+Consolidate development documentation to `docs/development/`.

docs/SUMMARY.md

@@ -67,7 +67,7 @@
 # Development
   - [Contributing Guide](development/contributing_guide.md)
   - [Code Style](code_style.md)
-  - [Git Usage](dev/git.md)
+  - [Git Usage](development/git.md)
   - [Testing]()
   - [OpenTracing](opentracing.md)
   - [Database Schemas](development/database_schema.md)
@@ -77,8 +77,8 @@
     - [TCP Replication](tcp_replication.md)
   - [Internal Documentation](development/internal_documentation/README.md)
     - [Single Sign-On]()
-      - [SAML](dev/saml.md)
-      - [CAS](dev/cas.md)
+      - [SAML](development/saml.md)
+      - [CAS](development/cas.md)
     - [State Resolution]()
       - [The Auth Chain Difference Algorithm](auth_chain_difference_algorithm.md)
     - [Media Repository](media_repository.md)

docs/dev/git.md → docs/development/git.md

@@ -9,7 +9,7 @@ commits each of which contains a single change building on what came
 before. Here, by way of an arbitrary example, is the top of `git log --graph
 b2dba0607`:
 
-<img src="git/clean.png" alt="clean git graph" width="500px">
+<img src="img/git/clean.png" alt="clean git graph" width="500px">
 
 Note how the commit comment explains clearly what is changing and why. Also
 note the *absence* of merge commits, as well as the absence of commits called
@@ -61,7 +61,7 @@ Ok, so that's what we'd like to achieve. How do we achieve it?
 The TL;DR is: when you come to merge a pull request, you *probably* want to
 “squash and merge”:
 
-![squash and merge](git/squash.png).
+![squash and merge](img/git/squash.png).
 
 (This applies whether you are merging your own PR, or that of another
 contributor.)
@@ -105,7 +105,7 @@ complicated. Here's how we do it.
 
 Let's start with a picture:
 
-![branching model](git/branches.jpg)
+![branching model](img/git/branches.jpg)
 
 It looks complicated, but it's really not. There's one basic rule: *anyone* is
 free to merge from *any* more-stable branch to *any* less-stable branch at