From a41c632291b017b47e2c40979ffc49b279442f3c Mon Sep 17 00:00:00 2001
From: Li Haoyi <haoyi.sg@gmail.com>
Date: Mon, 8 Jul 2019 08:03:34 +0800
Subject: make use of mill file if it exists and we're not already using it

---
 mill | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'mill')

diff --git a/mill b/mill
index 0e6cfd2a..e4b3424f 100755
--- a/mill
+++ b/mill
@@ -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
-- 
cgit v1.2.3