Fix date inset except on windows (bug 9925)

The important thing is actually not the date inset, but the converter
machinery, which did convert the time stamps of two unused freshly created
temp files, which does not make sense, and did work before f09a9fe2 only by
accident.
This fixes the date inset on linuy, but not on windows, probably due to
different file locking semantics.

diff --git a/src/insets/ExternalSupport.cpp b/src/insets/ExternalSupport.cpp
index b5afc0c1d913294b8c24fb9dbf274bafb1e9ffe6..cbbb88bc2b3e8cf6b076758fe749d1f3d6e38ee4 100644 (file)
--- a/src/insets/ExternalSupport.cpp
+++ b/src/insets/ExternalSupport.cpp
@@ -260,10 +260,11 @@ void updateExternal(InsetExternalParams const & params,
 
        // We copy the source file to the temp dir and do the conversion
        // there if necessary
+       bool const isDir = params.filename.isDirectory();
        FileName const temp_file(
                makeAbsPath(params.filename.mangledFileName(),
                                     masterBuffer->temppath()));
-       if (!params.filename.empty() && !params.filename.isDirectory()) {
+       if (!params.filename.empty() && !isDir) {
                unsigned long const from_checksum = params.filename.checksum();
                unsigned long const temp_checksum = temp_file.checksum();
 
@@ -320,7 +321,8 @@ void updateExternal(InsetExternalParams const & params,
 
        // Do we need to perform the conversion?
        // Yes if to_file does not exist or if from_file is newer than to_file
-       if (compare_timestamps(temp_file, abs_to_file) < 0)
+       // or if from_file is a directory (bug 9925)
+       if (!isDir && compare_timestamps(temp_file, abs_to_file) < 0)
                return; // SUCCESS
 
        // FIXME (Abdel 12/08/06): Is there a need to show these errors?