console: Add printk helper for ChromeOS

Do not expose console_tx_flush() to ChromeOS as that function
is part of lower-level implementation.

Change-Id: I1e31662da88a60e83f8e5d307a4b53441c130aab
Signed-off-by: Kyösti Mälkki <kyosti.malkki@gmail.com>
Reviewed-on: http://review.coreboot.org/5347
Tested-by: build bot (Jenkins)
Reviewed-by: Patrick Georgi <patrick@georgi-clan.de>

src/console/printk.c

@@ -40,3 +40,11 @@ int do_printk(int msg_level, const char *fmt, ...)
 
 	return i;
 }
+
+#if CONFIG_CHROMEOS
+void do_vtxprintf(const char *fmt, va_list args)
+{
+	vtxprintf(console_tx_byte, fmt, args);
+	console_tx_flush();
+}
+#endif