#!/bin/sh echo "/* Automatically generated by generate-configlist.sh */" echo print_config_list () { cat <