add "write_headers_string" to RESPONSE_BUFFER

2011-08-02 10:46:53 +02:00
parent e9085c614c
commit 10f4a99ee1
4 changed files with 25 additions and 4 deletions
--- a/library/server/ewsgi/specification/response/ewsgi_response_buffer.e
+++ b/library/server/ewsgi/specification/response/ewsgi_response_buffer.e
@@ -97,6 +97,16 @@ feature -- Output operation

 feature -- Header output operation

+	write_headers_string (a_headers: STRING)
+		require
+			status_set: status_is_set
+			header_not_committed: not header_committed
+		deferred
+		ensure
+			status_set: status_is_set
+			header_committed: header_committed
+		end
+
 	write_header (a_status_code: INTEGER; a_headers: detachable ARRAY [TUPLE [key: STRING; value: STRING]])
 			-- Send headers with status `a_status', and headers from `a_headers'
 		require