diff --git a/Makefile b/Makefile
index e37800845..503b9c548 100644
--- a/Makefile
+++ b/Makefile
@@ -37,7 +37,7 @@ build:
 	lake build
 
 # Select which commit of mathlib3 to use.
-MATHBIN_COMMIT=origin/master
+MATHBIN_COMMIT=origin/port-complete
 
 # Clone mathlib3 and create `all.lean`.
 mathbin-source:
diff --git a/README.md b/README.md
index a5409f3f1..86ab46c8d 100644
--- a/README.md
+++ b/README.md
@@ -35,7 +35,7 @@ In the mathport folder:
   all of the dependencies of tactics.
 - `make source`
 - `./download-release.sh`
-  (Or `./download-release.sh [relevant-release]`
+  (Or `./download-release.sh nightly-2023-07-22-09`
   if you need to run against an old mathlib;
   see [mathport releases](https://github.com/leanprover-community/mathport/releases),
   and find the nearest `nightly`.)
@@ -46,7 +46,7 @@ Similarly bump your mathlib dependency to the lastest mathlib3 if possible.
 
 If you really want to run against an older mathlib3 (good luck!):
 
-- In `sources/mathlib` run `git --fetch unshallow`
+- In `sources/mathlib` run `git fetch --unshallow`
 - `git checkout SHA` for the mathlib3 SHA you need.
 - `leanproject get-cache`
 
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,
diff --git a/lake-manifest.json b/lake-manifest.json
index fb52690a4..c859ee367 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -18,7 +18,7 @@
     "subDir?": null,
     "rev": "46f71c61691f26accd73c5ee411801d2d696bf0c",
     "name": "mathlib",
-    "inputRev?": "master"}},
+    "inputRev?": "port-complete"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,