Append ".gz" to filenames of gzip compressed files.
RELNOTES: None.
PiperOrigin-RevId: 282583739
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
index 7b13a12..c4e7686 100644
--- 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, 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;
}