doc: remove orphaned header in developer notes

The "Git and GitHub tips" section was moved from doc/developer-notes.md to doc/productivity.md in 5b76c31, but the header link to that long-gone section in the developer notes remains and needs to go.

So long, Git and GitHub tips, we barely knew ya.
This commit is contained in:
Jon Atack 2019-06-20 18:07:02 -04:00
parent 413e438ea9
commit 5a88ea7c67
No known key found for this signature in database
GPG key ID: 4F5721B3D0E3921D

View file

@ -34,7 +34,6 @@ Developer Notes
- [Source code organization](#source-code-organization)
- [GUI](#gui)
- [Subtrees](#subtrees)
- [Git and GitHub tips](#git-and-github-tips)
- [Scripted diffs](#scripted-diffs)
- [Release notes](#release-notes)
- [RPC interface guidelines](#rpc-interface-guidelines)