System.FilePath.parent did not return the correct parent path in the case of absolute file paths Example of previous behavior ``` (FilePath.mk "/foo").parent -> some (FilePath.mk "") (System.FilePath.mk "/").parent -> some (FilePath.mk "") ``` The new behavior is based on rust's std::path::Path::parent function (as previously described in comment in System.FilePath) Example of updated behavior ``` (System.FilePath.mk "/foo").parent -> some (FilePath.mk "/") (System.FilePath.mk "/").parent -> none ``` Behavior for relative file paths is unchanged Closes #3618 |
||
|---|---|---|
| .. | ||
| FilePath.lean | ||
| IO.lean | ||
| IOError.lean | ||
| Mutex.lean | ||
| Platform.lean | ||
| Promise.lean | ||
| ST.lean | ||
| Uri.lean | ||