mirror of
https://github.com/MariaDB/server.git
synced 2026-05-07 15:45:33 +02:00
don't allow to commit as mysqldev
This commit is contained in:
parent
2576beab6b
commit
c4ab5d61fb
1 changed files with 11 additions and 0 deletions
|
|
@ -1,5 +1,16 @@
|
|||
#!/bin/sh
|
||||
|
||||
if [ "$BK_USER" = "Administrator" -o "$BK_USER" = "mysqldev" ]
|
||||
then
|
||||
echo "Error: you cannot commit as 'Administrator' or 'mysqldev' user."
|
||||
echo "as a workaround set BK_USER to your nickname"
|
||||
echo "e.g.: export BK_USER='bar'"
|
||||
echo ""
|
||||
echo "Checkin FAILED!"
|
||||
echo "Set BK_USER and retry."
|
||||
exit 1
|
||||
fi
|
||||
|
||||
if [ "$REAL_EMAIL" = "" ]
|
||||
then
|
||||
echo "Error: you must set REAL_EMAIL in your profile"
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue