From 86ce2b40f66894b7248cc6ce4e88fb75d37a8cce Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 20 Jul 2023 09:45:33 +0100 Subject: [PATCH] Change the replacement style used for mathlib3port to `keep` These `#print`s and surrounding comments are annoying to remove when re-porting files, and having the declarations commented out isn't particularly useful anyway. The real motivation here is to make mathport produce a tree that is suitable for inserting between the mathlib3 and mathlib4 history, with ideally-minimal diffs --- config.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/config.json b/config.json index 1263fd69b..1e3ccbdc6 100644 --- a/config.json +++ b/config.json @@ -69,7 +69,7 @@ "sorries": [], "skipProofs": false, "skipDefEq": true, - "replacementStyle": "comment", + "replacementStyle": "keep", "redundantAlign": true, "error2warning" : true, "dubiousMsg": false,