max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: fix broken uri test (#12230)

Browse source
This commit is contained in:
Marc Huisinga 2026-01-29 14:52:36 +01:00 • committed by GitHub
parent e7b6bd6734
commit 30c8b39b23
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/Uri.lean
View file

@ -44,7 +44,7 @@ def testUnicodeEscape :=
true
def testRoundTrip :=
assert! (fileUriToPath? (pathToUri "/temp/test.xml?😵=2022")) == "/temp/test.xml?😵=2022"
assert! (fileUriToPath? (pathToUri ("" / "temp" / "test.xml?😵=2022")) == ("" / "temp" / "test.xml?😵=2022" : System.FilePath))
true
def testInvalidFileUri :=