diff --git a/doc/tools/make_rst.py b/doc/tools/make_rst.py index 746bfd199d4..6d08efb1f4d 100755 --- a/doc/tools/make_rst.py +++ b/doc/tools/make_rst.py @@ -321,7 +321,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":