From d190ad88af555bb2ee213aa64205f2b9a97a077d Mon Sep 17 00:00:00 2001 From: Colin Seymour Date: Wed, 14 Aug 2024 08:35:08 +0100 Subject: [PATCH] Manually remove module in `.git` when replacing grammars (#6990) --- script/add-grammar | 1 + 1 file changed, 1 insertion(+) diff --git a/script/add-grammar b/script/add-grammar index 92743fafcc..cc66cf0bec 100755 --- a/script/add-grammar +++ b/script/add-grammar @@ -123,6 +123,7 @@ if [ "$replace" ]; then log "Deregistering submodule: $replace" git submodule deinit "$replace" git rm -rf "$replace" + rm -rf ".git/modules/$replace" script/grammar-compiler update -f >/dev/null 2>&1 fi