# HG changeset patch
# User wenzelm
# Date 1544048455 -3600
# Node ID 7742cace5dd98be65731b522c363ad839387f15b
# Parent  5e5f1109c783ebd5d3d2f458514a2709f5655cb8
more robust: "gtar" is default name in Homebrew;

diff -r 5e5f1109c783 -r 7742cace5dd9 lib/scripts/getfunctions
--- a/lib/scripts/getfunctions	Wed Dec 05 23:15:23 2018 +0100
+++ b/lib/scripts/getfunctions	Wed Dec 05 23:20:55 2018 +0100
@@ -25,6 +25,10 @@
 then
   function tar() { gnutar "$@"; }
   export -f tar
+elif type -p gtar >/dev/null
+then
+  function tar() { gtar "$@"; }
+  export -f tar
 fi
 
 #OCaml management via OPAM