severity 8990 minor
severity 7229 minor
severity 24057 minor
merge 7229 8990 24057
quit

# Noam, looks like we were toggling the severities at the same time
# Hopefully, this finally does the merge :)

-- 

Kaushal Modi