use push(char) instead of push_str(&str) to add single chars to strings

clippy::single-char-push-str

compiler/rustc_session/src/config.rs

@@ -581,9 +581,9 @@ impl OutputFilenames {
 
         if !ext.is_empty() {
             if !extension.is_empty() {
-                extension.push_str(".");
+                extension.push('.');
                 extension.push_str(RUST_CGU_EXT);
-                extension.push_str(".");
+                extension.push('.');
             }
 
             extension.push_str(ext);