Fix bug #11750.

Unfortunately, stat.st_ino returns 0 on Windows, at least on Python 2.7, so we can't use that way of telling when we're seeing the same directory again. Surely the real pathname should work.

(cherry picked from commit 9d8dfe934ba6a73a899c907a687552104d2cb847)

diff --git a/lib/scripts/TeXFiles.py b/lib/scripts/TeXFiles.py
index 188f6b90ad64d6d16311a818b28d5e95c58cc081..16b7df2e8b2a2ec7e29bab2b4ba42b4a431e1931 100755 (executable)
--- a/lib/scripts/TeXFiles.py
+++ b/lib/scripts/TeXFiles.py
@@ -121,10 +121,11 @@ for type in types:
             # prevent inifinite recursion
             recurse = []
             for dir in dirs:
-                st = os.stat(os.path.join(root, dir))
-                key = st.st_dev, st.st_ino
-                if key not in visited:
-                    visited.add(key)
+                dirname = os.path.join(root, dir)
+                dirname = os.path.realpath(dirname)
+                dirname = os.path.normcase(dirname)
+                if dirname not in visited:
+                    visited.add(dirname)
                     recurse.append(dir)
             dirs[:] = recurse
             # check file type