From b49f4a1f6716ae491fcf3846fdb2d318dbe9e86f Mon Sep 17 00:00:00 2001
From: leanprover-community-bot <leanprover.community@gmail.com>
Date: Fri, 28 Jul 2023 01:11:24 +0000
Subject: [PATCH] bump to nightly-2023-07-28-01

mathlib commit https://github.com/leanprover-community/mathlib/commit/d11f435d4e34a6cea0a1797d6b625b0c170be845
---
 lake-manifest.json | 4 ++--
 lakefile.lean      | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 20a3c8179e..3a13a3e62b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "797ddae47e8459abb26f04c46358c50d1ab1691d",
+    "rev": "61d54fcf7b6afabc5b4fdc5867b261eb5ddd5fc4",
     "name": "lean3port",
-    "inputRev?": "797ddae47e8459abb26f04c46358c50d1ab1691d"}},
+    "inputRev?": "61d54fcf7b6afabc5b4fdc5867b261eb5ddd5fc4"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index f34fd04ddb..6a80d1376c 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-07-27-23"
+def tag : String := "nightly-2023-07-28-01"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"797ddae47e8459abb26f04c46358c50d1ab1691d"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"61d54fcf7b6afabc5b4fdc5867b261eb5ddd5fc4"
 
 @[default_target]
 lean_lib Mathbin where