Mercurial > hg > Gears > GearsAgda
view .git/hooks/pre-receive.sample @ 956:bfc7007177d0 default tip
safe and cubical compatible with no warning done
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 19 Oct 2024 09:48:48 +0900 (2024-10-19) |
parents | 68904fdaab71 |
children |
line wrap: on
line source
#!/bin/sh # # An example hook script to make use of push options. # The example simply echoes all push options that start with 'echoback=' # and rejects all pushes when the "reject" push option is used. # # To enable this hook, rename this file to "pre-receive". if test -n "$GIT_PUSH_OPTION_COUNT" then i=0 while test "$i" -lt "$GIT_PUSH_OPTION_COUNT" do eval "value=\$GIT_PUSH_OPTION_$i" case "$value" in echoback=*) echo "echo from the pre-receive-hook: ${value#*=}" >&2 ;; reject) exit 1 esac i=$((i + 1)) done fi