From 8ba988ed7fd4f88590de57ca5bb73bcc72640259 Mon Sep 17 00:00:00 2001
From: Petr Baudis <pasky@ucw.cz>
Date: Tue, 10 Oct 2006 02:48:35 +0200
Subject: [PATCH] Warn that adjusting user set for mirrored repositories has no
 effect

---
 cgi/p/editproj.cgi | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/cgi/p/editproj.cgi b/cgi/p/editproj.cgi
index 6746926..a80c698 100755
--- a/cgi/p/editproj.cgi
+++ b/cgi/p/editproj.cgi
@@ -56,6 +56,9 @@ so perhaps you will need to click a lot.</p>
 <p>Users:</p>
 <ul>
 EOT
+if ($repo->{mirror}) {
+	print "<p><em>Warning: This is a mirroring repository, thus you cannot push into it. Changing the user set will have no practical effect.</em></p>\n";
+}
 foreach my $user (@{$h{users}}) {
 	print "<li><input type=\"checkbox\" name=\"user\" value=\"$user\" checked=\"1\" /> $user</li>\n";
 }
-- 
2.11.4.GIT