config: Rename push.branch-prefix option to git.push-branch-prefix

This is for consistency with other `git.` options. See also
https://github.com/martinvonz/jj/pull/1962#discussion_r1282605185

CHANGELOG.md

@@ -25,6 +25,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   used for allowing duplicate destinations. Include the potential duplicates
   in a single expression instead (e.g. `jj new 'all:x|y'`).
 
+* The `push.branch-prefix` option was renamed to `git.push-branch-prefix`.
+
 ### New features
 
 * `jj init --git-repo` now works with bare repositories.

cli/src/config-schema.json

@@ -32,16 +32,6 @@
                 }
             }
         },
-        "push": {
-            "type": "object",
-            "properties": {
-                "branch-prefix": {
-                    "type": "string",
-                    "description": "Prefix used when pushing a change ID as a new branch",
-                    "default": "push-"
-                }
-            }
-        },
         "ui": {
             "type": "object",
             "description": "UI settings",
@@ -215,6 +205,11 @@
                     "description": "Whether jj creates a local branch with the same name when it imports a remote-tracking branch from git. See https://github.com/martinvonz/jj/blob/main/docs/config.md#automatic-local-branch-creation",
                     "default": true
                 },
+                "push-branch-prefix": {
+                    "type": "string",
+                    "description": "Prefix used when pushing a change ID as a new branch",
+                    "default": "push-"
+                },
                 "fetch": {
                     "description": "The remote(s) from which commits are fetched",
                     "default": "origin",

docs/config.md

@@ -475,10 +475,10 @@ deleted if you push the branch with `jj git push --branch` or `jj git push
 ### Prefix for generated branches on push
 
 `jj git push --change` generates branch names with a prefix of "push-" by
-default. You can pick a different prefix by setting `push.branch-prefix`. For
+default. You can pick a different prefix by setting `git.push-branch-prefix`. For
 example:
 
-    push.branch-prefix = "martinvonz/push-"
+    git.push-branch-prefix = "martinvonz/push-"
 
 ## Filesystem monitor
 

lib/src/settings.rs

@@ -142,7 +142,7 @@ impl UserSettings {
 
     pub fn push_branch_prefix(&self) -> String {
         self.config
-            .get_string("push.branch-prefix")
+            .get_string("git.push-branch-prefix")
             .unwrap_or_else(|_| "push-".to_string())
     }