From 314a739160effac7501201cadfc8aaa9c4f34713 Mon Sep 17 00:00:00 2001 From: David Robertson Date: Thu, 12 Aug 2021 10:40:32 +0100 Subject: [PATCH] Also rename in lint.sh --- scripts-dev/lint.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts-dev/lint.sh b/scripts-dev/lint.sh index 2c77643cd..809eff166 100755 --- a/scripts-dev/lint.sh +++ b/scripts-dev/lint.sh @@ -94,7 +94,7 @@ else "scripts-dev/build_debian_packages" "scripts-dev/sign_json" "scripts-dev/update_database" - "contrib" "synctl" "setup.py" "synmark" "stubs" "ci" + "contrib" "synctl" "setup.py" "synmark" "stubs" ".ci" ) fi fi