From 5a88ea7c67448748a63ac7963c70a047a5daca79 Mon Sep 17 00:00:00 2001 From: Jon Atack Date: Thu, 20 Jun 2019 18:07:02 -0400 Subject: [PATCH] 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. --- doc/developer-notes.md | 1 - 1 file changed, 1 deletion(-) diff --git a/doc/developer-notes.md b/doc/developer-notes.md index f4fc55427d9..ecd720539e7 100644 --- a/doc/developer-notes.md +++ b/doc/developer-notes.md @@ -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)