diff options
author | Li Haoyi <haoyi.sg@gmail.com> | 2019-07-08 08:03:34 +0800 |
---|---|---|
committer | Li Haoyi <haoyi.sg@gmail.com> | 2019-07-08 08:07:36 +0800 |
commit | a41c632291b017b47e2c40979ffc49b279442f3c (patch) | |
tree | 2789f093c59f703e14127e1bb3af45cf415f3ce6 /mill | |
parent | de1e0e4ae3ef0b65075c9896ea25a9b23e2376ee (diff) | |
download | mill-a41c632291b017b47e2c40979ffc49b279442f3c.tar.gz mill-a41c632291b017b47e2c40979ffc49b279442f3c.tar.bz2 mill-a41c632291b017b47e2c40979ffc49b279442f3c.zip |
make use of mill file if it exists and we're not already using it
Diffstat (limited to 'mill')
-rwxr-xr-x | mill | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -10,6 +10,8 @@ set -e if [ -z "$MILL_VERSION" ] ; then if [ -f ".mill-version" ] ; then MILL_VERSION="$(head -n 1 .mill-version 2> /dev/null)" + elif [ -f "mill" ] && [ "$BASH_SOURCE" != "mill" ] ; then + MILL_VERSION=$(grep -F "DEFAULT_MILL_VERSION=" "mill" | cut -d= -f2) else MILL_VERSION=$DEFAULT_MILL_VERSION fi |