push: Do not use push options unless requested

Unless the user passed --push-option, the client does not intend to
pass push options to the server.

Without this change, all pushes to servers without push option support
fail.

Not enabling the feature (instead of enabling it and sending an empty
list of options) in this case is more intuitive and matches the
behavior of C git push's --push-option parameter better.

Bug: 500149
Change-Id: Ia4f13840cc54d8ba54e99b1432108f1c43022c53
Signed-off-by: Stefan Beller <sbeller@google.com>

org.eclipse.jgit.pgm/src/org/eclipse/jgit/pgm/Push.java

@@ -130,7 +130,9 @@ class Push extends TextBuiltin {
 			push.setThin(thin);
 			push.setAtomic(atomic);
 			push.setTimeout(timeout);
+			if (!pushOptions.isEmpty()) {
 				push.setPushOptions(pushOptions);
+			}
 			Iterable<PushResult> results = push.call();
 			for (PushResult result : results) {
 				try (ObjectReader reader = db.newObjectReader()) {