From 9937a1660e3a7cc381df9e3cfc26ec9100892244 Mon Sep 17 00:00:00 2001
From: Alexey Radul <axch@google.com>
Date: Fri, 21 Oct 2022 12:09:23 -0400
Subject: [PATCH] Ignore the preceding commit in blame history, being a
 formatting change.

---
 .git-blame-ignore-revs | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 .git-blame-ignore-revs

diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
new file mode 100644
index 000000000..04e001e72
--- /dev/null
+++ b/.git-blame-ignore-revs
@@ -0,0 +1,5 @@
+# Run this command to always ignore these in local `git blame`:
+# git config blame.ignoreRevsFile .git-blame-ignore-revs
+
+# Formatted TopLevel.hs to 80 character width
+ef500cc06f96bddcc355d0e29945a3d48dd19867