chore: forward-port leanprover-community/mathlib#19134 (#4581)

The mathlib3 change was fixing a synchronization comment, so there is nothing to port.
leanprover-community · Jun 2, 2023 · 9523725 · 9523725
1 parent 204f135
commit 9523725
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Analysis/NormedSpace/PiLp.lean b/Mathlib/Analysis/NormedSpace/PiLp.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Jireh Loreaux
 
 ! This file was ported from Lean 3 source module analysis.normed_space.pi_Lp
-! leanprover-community/mathlib commit 13bce9a6b6c44f6b4c91ac1c1d2a816e2533d395
+! leanprover-community/mathlib commit 9d013ad8430ddddd350cff5c3db830278ded3c79
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/