kernel/configure

#!/bin/sh -e

ENV="$1"

if [ -z "$ENV" ]; then
    ENV='build'
fi

CONFIG="env/$ENV.mk"

if [ ! -f "$CONFIG" ]; then
    echo >&2 "ERROR: file "$CONFIG" does not exist"
    exit 1
fi

cp "$CONFIG" 'config.mk'