#!/bin/sh

sed '/^\(#+html: *<hr\/>\)$/d' src/en/index.org > src/en/index-filtered.org