mirrors/EWF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Applied recent renaming from WGI_RESPONSE_BUFFER as WGI_RESPONSE

Browse Source
This commit is contained in:
Jocelyn Fiat
2011-11-25 19:21:45 +01:00
parent 2234d3712b
commit e0ec84611e
2 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
library/server/ewsgi/examples/hello_world/src/hello_world.e
View File

@@ -18,7 +18,7 @@ feature {NONE} -- Initialization
(create {NINO_SERVICE}.make_custom (agent execute, "")).listen (port_number) (create {NINO_SERVICE}.make_custom (agent execute, "")).listen (port_number)
end end
execute (req: WGI_REQUEST; res: WGI_RESPONSE_BUFFER) execute (req: WGI_REQUEST; res: WGI_RESPONSE)
do do
res.write_header (200, <<["Content-Type", "text/plain"]>>) res.write_header (200, <<["Content-Type", "text/plain"]>>)
res.write_string ("Hello World!%N") res.write_string ("Hello World!%N")

2
library/server/ewsgi/specification/response/wgi_response.e
View File

@@ -34,7 +34,7 @@ feature -- Status report
deferred deferred
end end
feature {WGI_RESPONSE_BUFFER} -- Core output operation feature {WGI_RESPONSE} -- Core output operation
write (s: READABLE_STRING_8) write (s: READABLE_STRING_8)
-- Send the string `s' -- Send the string `s'