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.

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