From ca57afd67ecf68a83ecd1bec9b7058b4cf3f2bae Mon Sep 17 00:00:00 2001 From: Christian Helmuth Date: Wed, 1 Mar 2017 17:19:46 +0100 Subject: [PATCH] terminal_crosslink: prevent deprecated warning --- repos/os/src/server/terminal_crosslink/terminal_root.h | 1 - 1 file changed, 1 deletion(-) diff --git a/repos/os/src/server/terminal_crosslink/terminal_root.h b/repos/os/src/server/terminal_crosslink/terminal_root.h index 35c123f904..0d3f5039ad 100644 --- a/repos/os/src/server/terminal_crosslink/terminal_root.h +++ b/repos/os/src/server/terminal_crosslink/terminal_root.h @@ -15,7 +15,6 @@ #define _TERMINAL_ROOT_H_ /* Genode includes */ -#include #include /* local includes */