Merge pull request #52 from colin-adams/master

Bad postcondition for handle_use_proxy
This commit is contained in:
Jocelyn Fiat
2013-04-08 09:24:38 -07:00

View File

@@ -260,7 +260,6 @@ feature {NONE} -- Implementation
ensure ensure
response_status_is_set: res.status_is_set response_status_is_set: res.status_is_set
response_code_use_proxy: res.status_code = {HTTP_STATUS_CODE}.use_proxy response_code_use_proxy: res.status_code = {HTTP_STATUS_CODE}.use_proxy
header_sent: res.header_committed and res.message_committed
end end
invariant invariant