From c8efa04147d28a648fe6a5062d7074b84287e5f8 Mon Sep 17 00:00:00 2001 From: Jocelyn Fiat Date: Thu, 15 Dec 2011 23:52:53 +0100 Subject: [PATCH] Use put_ instead of write_ --- library/server/ewsgi/examples/hello_world/src/hello_world.e | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/server/ewsgi/examples/hello_world/src/hello_world.e b/library/server/ewsgi/examples/hello_world/src/hello_world.e index 5d9efa27..42a302da 100644 --- a/library/server/ewsgi/examples/hello_world/src/hello_world.e +++ b/library/server/ewsgi/examples/hello_world/src/hello_world.e @@ -21,8 +21,8 @@ feature {NONE} -- Initialization execute (req: WGI_REQUEST; res: WGI_RESPONSE) do res.set_status_code (200) - res.write_header_lines (<<["Content-Type", "text/plain"]>>) - res.write_string ("Hello World!%N") + res.put_header_lines (<<["Content-Type", "text/plain"]>>) + res.put_string ("Hello World!%N") end port_number: INTEGER = 8123