echo "writing generated aliases in $GENERATED_ALIAS_FILE..."
#hmmm: perhaps a good place for a function to create the header,
echo "writing generated aliases in $GENERATED_ALIAS_FILE..."
#hmmm: perhaps a good place for a function to create the header,