diff options
Diffstat (limited to 'doc/tools')
| -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": |