Properly name an uncompressed sgvz file.

Some tools may rely on the extension and do not actually check whether
a svg file is compressed or not.

diff --git a/src/support/filetools.cpp b/src/support/filetools.cpp
index 20088386f943a5b4559c77f1ae1eb5ceb7baa4d0..134dc1756101ac2d8ad27aeecbfc36db33e244d0 100644 (file)
--- a/src/support/filetools.cpp
+++ b/src/support/filetools.cpp
@@ -872,6 +872,8 @@ string const unzippedFileName(string const & zipped_file)
        string const ext = getExtension(zipped_file);
        if (ext == "gz" || ext == "z" || ext == "Z")
                return changeExtension(zipped_file, string());
+       else if (ext == "svgz")
+               return changeExtension(zipped_file, "svg");
        return onlyPath(zipped_file) + "unzipped_" + onlyFileName(zipped_file);
 }