diff options
| author | Rémi Verschelde <remi@verschelde.fr> | 2022-01-24 12:03:04 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-01-24 12:03:04 +0100 |
| commit | 6a3ff8fa1f2cbad5752cf039827206ac265f68f6 (patch) | |
| tree | e8ea5cd281b30aa1796cbbd223dc64505cb312b8 | |
| parent | e8789132b46dd9bec6fcfad8d578e5f869fb7326 (diff) | |
| parent | 26da72eb4b37c70e4306524dd843ef21f692e455 (diff) | |
Merge pull request #57112 from mhilbrunner/docs-fixes-main
| -rwxr-xr-x | doc/tools/make_rst.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tools/make_rst.py b/doc/tools/make_rst.py index 9e18866ca3..68f3b66f43 100755 --- a/doc/tools/make_rst.py +++ b/doc/tools/make_rst.py @@ -438,7 +438,7 @@ def main(): # type: () -> None for path in args.path: # Cut off trailing slashes so os.path.basename doesn't choke. - if path.endswith(os.sep): + if path.endswith("/") or path.endswith("\\"): path = path[:-1] if os.path.basename(path) == "modules": |