From d8476edf369326e8d7f2f2f0bb5649142d43b093 Mon Sep 17 00:00:00 2001 From: Jocelyn Fiat Date: Wed, 1 Feb 2012 16:53:24 +0100 Subject: [PATCH] Fixed wrong code for postcondition on HTTP_HEADER.string Patch provided by Paul-G.Crismer --- library/protocol/http/src/http_header.e | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/protocol/http/src/http_header.e b/library/protocol/http/src/http_header.e index 9bdb0984..346dc871 100644 --- a/library/protocol/http/src/http_header.e +++ b/library/protocol/http/src/http_header.e @@ -116,8 +116,8 @@ feature -- Access create Result.make_empty end ensure - result_has_ending_cr_lf: Result.count >= 2 implies Result.substring (Result.count - 2, Result.count).same_string ("%R%N") - result_has_single_ending_cr_lf: Result.count >= 4 implies not Result.substring (Result.count - 4, Result.count).same_string ("%R%N%R%N") + result_has_ending_cr_lf: Result.count >= 2 implies Result.substring (Result.count - 1, Result.count).same_string ("%R%N") + result_has_single_ending_cr_lf: Result.count >= 4 implies not Result.substring (Result.count - 3, Result.count).same_string ("%R%N%R%N") end feature -- Header change: general