Append ".gz" to filenames of gzip compressed files.

RELNOTES: None. PiperOrigin-RevId: 282583739
bazelbuild · Nov 26, 2019 · 48957db · 48957db
1 parent 40c1123
commit 48957db
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/src/main/java/com/google/devtools/build/lib/buildtool/BuildResult.java b/src/main/java/com/google/devtools/build/lib/buildtool/BuildResult.java
@@ -335,6 +335,13 @@ public BuildToolLogCollection addLocalFile(String name, Path path) {
     public BuildToolLogCollection addLocalFile(
         String name, Path path, LocalFileType localFileType, LocalFileCompression compression) {
       Preconditions.checkState(!frozen);
+      switch (compression) {
+        case GZIP:
+          name = name + ".gz";
+          break;
+        case NONE:
+          break;
+      }
       this.localFiles.add(new LogFileEntry(name, path, localFileType, compression));
       return this;
     }