mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
fix: port and fragment
This commit is contained in:
@@ -892,14 +892,6 @@ def authority? : RequestTarget → Option URI.Authority
|
||||
| .absoluteForm u _ => u.authority
|
||||
| _ => none
|
||||
|
||||
/--
|
||||
Extracts the fragment component from a request target, if available.
|
||||
-/
|
||||
def fragment? : RequestTarget → Option String
|
||||
| .originForm _ _ => none
|
||||
| .absoluteForm u _ => u.fragment
|
||||
| _ => none
|
||||
|
||||
/--
|
||||
Extracts the full URI if the request target is in absolute form.
|
||||
-/
|
||||
|
||||
Reference in New Issue
Block a user