From 74d99709087151d4d2eff1f802e26cd07a587774 Mon Sep 17 00:00:00 2001
From: Ilya Grigoriev <ilyagr@users.noreply.github.com>
Date: Mon, 7 Aug 2023 15:36:39 -0700
Subject: [PATCH] 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               |  2 ++
 cli/src/config-schema.json | 15 +++++----------
 docs/config.md             |  4 ++--
 lib/src/settings.rs        |  2 +-
 4 files changed, 10 insertions(+), 13 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4fa45dff8..51e1bef6e 100644
--- a/CHANGELOG.md
+++ b/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.
diff --git a/cli/src/config-schema.json b/cli/src/config-schema.json
index e4e336301..bbeaaca8b 100644
--- a/cli/src/config-schema.json
+++ b/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",
diff --git a/docs/config.md b/docs/config.md
index 813407ac1..03f8c52cf 100644
--- a/docs/config.md
+++ b/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
 
diff --git a/lib/src/settings.rs b/lib/src/settings.rs
index 2b24e502b..e279453db 100644
--- a/lib/src/settings.rs
+++ b/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())
     }