rust/rhg/src/ui.rs
changeset 45451 a6a000ab135b
parent 45450 fbc373b7cbc3
child 45534 66756b34c06e
--- a/rust/rhg/src/ui.rs	Thu Aug 13 16:36:42 2020 +0200
+++ b/rust/rhg/src/ui.rs	Mon Aug 17 16:55:43 2020 +0200
@@ -47,6 +47,11 @@
 
         stderr.flush().or_else(handle_stderr_error)
     }
+
+    /// Write string line to stderr
+    pub fn writeln_stderr_str(&self, s: &str) -> Result<(), UiError> {
+        self.write_stderr(&format!("{}\n", s).as_bytes())
+    }
 }
 
 /// A buffered stdout writer for faster batch printing operations.