From 80af39824b9cd90a4260098b5ed5fc0c8cb59930 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Edouard=20Choini=C3=A8re?=
 <27212526+echoix@users.noreply.github.com>
Date: Tue, 28 Nov 2023 19:03:36 -0500
Subject: [PATCH] Remove outdated section about ignore-revs on GitHub in
 investigating_history.md

---
 doc/git/investigating_history.md | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/doc/git/investigating_history.md b/doc/git/investigating_history.md
index 0e62f731958..306b4fe819c 100644
--- a/doc/git/investigating_history.md
+++ b/doc/git/investigating_history.md
@@ -27,9 +27,3 @@ In some cases, ignoring formatting changes may not be appropriate, for example
 when investigating automated checks of formatting.
 If you think the _ignore-revs_ file contains commits which should be never
 ignored with `git blame`, please open an issue.
-
-## On GitHub
-
-GitHub interface does not allow to use the ignore-revs file. However, it is
-easy to move over a revision by pressing "View blame prior to this change"
-which is the icon between commit info and line numbers.