#! /bin/bash
set -e

scriptdir=$(dirname "$0")
flints="${scriptdir}/index/default"
options=optionlist

"${scriptdir}/index-list-optionlist" > "${options}.new-$$"
mv "${options}.new-$$" "${options}"

"${scriptdir}/index-list-flintlist" > "${flints}.new-$$"
mv "${flints}.new-$$" "${flints}"


