From 61122401d553b5976ee5e7144d44e84dd1bb3d5c Mon Sep 17 00:00:00 2001
From: Magnus Jacobsson <magnus.jacobsson@berotec.se>
Date: Sun, 20 Sep 2020 21:50:06 +0200
Subject: [PATCH] Add option -? for usage to non-Windows version of dotty

---
 cmd/dotty/dotty.sh | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/cmd/dotty/dotty.sh b/cmd/dotty/dotty.sh
index b3789567d..86ed4c8b5 100755
--- a/cmd/dotty/dotty.sh
+++ b/cmd/dotty/dotty.sh
@@ -45,6 +45,10 @@ while [ "x$1" != 'x' ]; do
         FILES=`echo $FILES \"$1\"`
         shift
         ;;
+    -\?)
+        $usage
+        exit 0
+        ;;
     -*)
         $usage
         exit 1
-- 
2.40.0