Cleanup of API of RichFutureUtils
Some minor cleanup of newly added classes to RichFutureUtils.
Can only be merged once Rec!1818 (merged) has been merged.
Edited by Christopher Rob Jones
Some minor cleanup of newly added classes to RichFutureUtils.
Can only be merged once Rec!1818 (merged) has been merged.