Removed incorrect postcondition for handle_use_proxy
This commit is contained in:
@@ -261,7 +261,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
|
||||||
|
|||||||
Reference in New Issue
Block a user