From 821584b8fc0b00730af323551a87bd8ca5bacba1 Mon Sep 17 00:00:00 2001
From: Anders Kaseorg <anders@zulip.com>
Date: Fri, 3 Mar 2023 17:18:26 -0800
Subject: [PATCH] gitlint-rules: Rename to gitlint_rules.

Signed-off-by: Anders Kaseorg <anders@zulip.com>
---
 .gitlint                                         | 2 +-
 tools/lib/{gitlint-rules.py => gitlint_rules.py} | 0
 2 files changed, 1 insertion(+), 1 deletion(-)
 rename tools/lib/{gitlint-rules.py => gitlint_rules.py} (100%)

diff --git a/.gitlint b/.gitlint
index 14ea524644..e419392d9a 100644
--- a/.gitlint
+++ b/.gitlint
@@ -1,7 +1,7 @@
 [general]
 ignore=title-trailing-punctuation, body-min-length, body-is-missing
 
-extra-path=tools/lib/gitlint-rules.py
+extra-path=tools/lib/gitlint_rules.py
 
 [title-match-regex]
 regex=^(.+:\ )?[A-Z].+\.$
diff --git a/tools/lib/gitlint-rules.py b/tools/lib/gitlint_rules.py
similarity index 100%
rename from tools/lib/gitlint-rules.py
rename to tools/lib/gitlint_rules.py