Use put_ instead of write_

2011-12-15 23:52:53 +01:00
parent 37860f43b5
commit c8efa04147
1 changed files with 2 additions and 2 deletions
--- 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