# This is a -*- shell-script -*- that used to be sourced by configure
# Intentionally empty now