From 7da3bf98fd64ac1e78b703642267ac2a32f10da4 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Thu, 2 Nov 2023 06:45:52 -0400
Subject: [PATCH] chore: test patch for std4#198

Remove this commit before merging
---
 lake-manifest.json | 16 ++++++++--------
 lakefile.lean      |  2 +-
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 2745fede3a98e..0cf3a3ba70293 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -2,14 +2,6 @@
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "fb43b83c13d10b90299d10d96512d20d33daa658",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": false}},
-  {"git":
    {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
     "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
@@ -40,5 +32,13 @@
     "opts": {},
     "name": "Cli",
     "inputRev?": "main",
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/fgdorais/std4",
+    "subDir?": null,
+    "rev": "cea56f69275f6a2ee8e263989cc69498f7a3854b",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "nat-mul",
     "inherited": false}}],
  "name": "mathlib"}
diff --git a/lakefile.lean b/lakefile.lean
index 602c5f200b068..a309057a7db4e 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -46,7 +46,7 @@ lean_exe checkYaml where
 meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
-require std from git "https://github.com/leanprover/std4" @ "main"
+require std from git "https://github.com/fgdorais/std4" @ "nat-mul"
 require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
 require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
 require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"