#! /bin/sh # @configure_input@ # WARNING: # WARNING: If you change the description, also change specgen.sh! # WARNING: cat <