#384 has also been merged into #389, so we should either remove it both places or leave it in both places. (I also think we should leave it in.)