Added FEED.prune (a_item: FEED_ITEM).

This commit is contained in:
2015-10-14 17:40:38 +02:00
parent 66f204b1f2
commit 061e88c9fe

View File

@@ -108,6 +108,12 @@ feature -- Element change
items.force (a_item) items.force (a_item)
end end
prune (a_item: FEED_ITEM)
-- Remove feed item `a_item' from Current list of feed items.
do
items.prune (a_item)
end
extended alias "+" (a_feed: FEED): FEED extended alias "+" (a_feed: FEED): FEED
-- New feed object made from Current merged with a_feed. -- New feed object made from Current merged with a_feed.
local local