From edfa03f0171b07e617ea2364ec8367d1c03d00c2 Mon Sep 17 00:00:00 2001
From: Samuel Tardieu <sam@rfc1149.net>
Date: Fri, 3 Feb 2023 00:20:07 +0100
Subject: [PATCH] config: add schema for git.push configuration entry

---
 src/commands/config-schema.json | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/commands/config-schema.json b/src/commands/config-schema.json
index 26bf7fa95..4c5dd3734 100644
--- a/src/commands/config-schema.json
+++ b/src/commands/config-schema.json
@@ -195,6 +195,11 @@
                             }
                         }
                     ]
+                },
+                "push": {
+                    "type": "string",
+                    "description": "The remote to which commits are pushed",
+                    "default": "origin"
                 }
             }
         },