hw: fix raw output functions for kernel

Ref #2092

repos/base-hw/lib/mk/base-hw.mk

@@ -4,5 +4,6 @@ SRC_CC += thread_start.cc
 SRC_CC += env.cc
 SRC_CC += capability.cc
 SRC_CC += cache.cc
+SRC_CC += raw_write_string.cc
 
 LIBS += startup-hw base-hw-common

repos/base-hw/src/core/core_log.cc

@@ -17,6 +17,7 @@
 
 /* base-internal includes */
 #include <base/internal/output.h>
+#include <base/internal/raw_write_string.h>
 #include <base/internal/unmanaged_singleton.h>
 
 #include <core_log.h>
@@ -44,3 +45,7 @@ void Genode::Core_log::out(char const c) { out_char(c); }
 
 
 void Kernel::log(char const c) { out_char(c); }
+
+
+void Genode::raw_write_string(char const *str) {
+	while (char c = *str++) out_char(c); }

repos/base-hw/src/include/base/internal/raw_write_string.h

@@ -14,15 +14,6 @@
 #ifndef _INCLUDE__BASE__INTERNAL__RAW_WRITE_STRING_H_
 #define _INCLUDE__BASE__INTERNAL__RAW_WRITE_STRING_H_
 
-#include <kernel/interface.h>
-
-namespace Genode {
-
-	void raw_write_string(char const *str)
-	{
-		while (char c = *str++)
-			Kernel::print_char(c);
-	}
-}
+namespace Genode { void raw_write_string(char const *str); }
 
 #endif /* _INCLUDE__BASE__INTERNAL__RAW_WRITE_STRING_H_ */

repos/base-hw/src/lib/base/raw_write_string.cc

@@ -0,0 +1,18 @@
+/*
+ * \brief  Kernel-specific raw-output back end
+ * \author Norman Feske
+ * \date   2016-03-08
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#include <kernel/interface.h>
+#include <base/internal/raw_write_string.h>
+
+void Genode::raw_write_string(char const *str) {
+	while (char c = *str++) Kernel::print_char(c); }