diff --git a/tlatools/test/util/SimpleFilenameToStreamTest.java b/tlatools/test/util/SimpleFilenameToStreamTest.java index 815e8db3429dd7f35de3e25e7bb9b63971bea5b1..18322e3bfaec3c95c7695d3a874f6c185c516d83 100644 --- a/tlatools/test/util/SimpleFilenameToStreamTest.java +++ b/tlatools/test/util/SimpleFilenameToStreamTest.java @@ -20,4 +20,22 @@ public class SimpleFilenameToStreamTest { assertNotNull(file); assertTrue(file.getAbsolutePath() + " does not exist!", file.exists()); } + + /** + * Test whether the fix for #424 still works + */ + @Test + public void testWindowsTLAFileCreation() { + if (System.getProperty("os.name").toLowerCase().indexOf("win") > -1) { + final String driveLetter = "X:"; + final String parentDirectory = driveLetter + "\\Develop\\myspecs\\DecentSpec\\"; + final String child = parentDirectory + "Fromage.tla"; + final FilenameToStream.TLAFile file = new FilenameToStream.TLAFile(parentDirectory, child, null); + final int driveLetterCount = file.getAbsolutePath().split(driveLetter).length - 1; + + assertTrue("There should be 1 drive letter in the child's absolute path, but there are " + driveLetterCount, + (1 == driveLetterCount)); + } + } + }