Manually remove module in .git when replacing grammars (github-ling…

…uist#6990)
manifoldfinance · Aug 14, 2024 · d190ad8 · d190ad8
1 parent 39fd5e9
commit d190ad8
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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