Ignore empty header line.

This commit is contained in:
2016-08-05 11:28:59 +02:00
parent c88394b9fd
commit cc2d7dbb1c

View File

@@ -180,7 +180,9 @@ feature -- Header: adding
if line [line.count] = '%R' then
line.remove_tail (1)
end
add_header (line)
if not line.is_empty then
add_header (line)
end
end
end
end