diff --git a/README.md b/README.md
index 09ddd486..a4494b29 100644
--- a/README.md
+++ b/README.md
@@ -221,14 +221,24 @@ Once you finish the installation, follow these steps:
 
 - Create a repository on GitLab.com which will be used to run CI jobs.
 
-  The bot will only take care of mirroring the PRs and reporting
-  status checks back so you may still want to activate the mirroring
-  feature for the main branches.  To do so, the easiest way is to
-  choose the "CI/CD for external repo" option when creating the GitLab
-  repository.  However, you should opt to give the repo by URL rather
-  than with the GitHub button, because we won't need GitLab's own
-  status check reporting feature. (If it is already activated, you can
-  disable this integration in the "Settings" / "Integration" menu).
+  By default, the bot will only take care of mirroring the PRs and
+  reporting status checks back. So you may still want to activate:
+
+  - either GitLab's mirroring feature for the main branches.
+    (A drawback is the
+    [sync lag](https://docs.gitlab.com/ee/user/project/repository/mirror/#update-a-mirror)
+    (between 5' and 30') that occurs with this pull-based mirroring.)
+    If you do so, the easiest way is to choose the "CI/CD for external
+    repo" option when creating the GitLab repository.  However, you
+    should opt to give the repo by URL rather than with the GitHub
+    button, because we won't need GitLab's own status check reporting
+    feature. (If it is already activated, you can disable this
+    integration in the "Settings" / "Integration" menu).
+
+  - or **@coqbot**'s mirroring feature (it is a push-based mirroring).
+    For now, this requires hardcoding the GitHub / GitLab mapping in
+    the bot's source code.  Please open an issue if you would like to
+    use this feature. We plan to make this configurable in the future.
 
 - In your GitLab repository:
 
diff --git a/bot-components/GitHub_subscriptions.ml b/bot-components/GitHub_subscriptions.ml
index 103524e2..0d19619e 100644
--- a/bot-components/GitHub_subscriptions.ml
+++ b/bot-components/GitHub_subscriptions.ml
@@ -143,11 +143,12 @@ let push_event_info_of_json json =
   in
   let repo = json |> member "repository" |> member "name" |> to_string in
   let base_ref = json |> member "ref" |> to_string in
+  let head_sha = json |> member "after" |> to_string in
   let commits = json |> member "commits" |> to_list in
   let commits_msg =
     List.map commits ~f:(fun c -> c |> member "message" |> to_string)
   in
-  {owner; repo; base_ref; commits_msg}
+  {owner; repo; base_ref; head_sha; commits_msg}
 
 type msg =
   | IssueOpened of issue_info
diff --git a/bot-components/GitHub_types.mli b/bot-components/GitHub_types.mli
index 15408b02..1301d053 100644
--- a/bot-components/GitHub_types.mli
+++ b/bot-components/GitHub_types.mli
@@ -85,7 +85,11 @@ type comment_info =
   ; id: GitHub_ID.t }
 
 type push_info =
-  {owner: string; repo: string; base_ref: string; commits_msg: string list}
+  { owner: string
+  ; repo: string
+  ; base_ref: string
+  ; head_sha: string
+  ; commits_msg: string list }
 
 type check_run_status = COMPLETED | IN_PROGRESS | QUEUED
 
diff --git a/src/actions.ml b/src/actions.ml
index 5c3f9751..51fd77bf 100644
--- a/src/actions.ml
+++ b/src/actions.ml
@@ -2289,6 +2289,30 @@ let remove_labels_if_present ~bot_info (issue : issue_info) labels =
     |> add_remove_labels ~bot_info ~add:false issue )
   |> Lwt.async
 
+(* TODO: ensure there's no race condition for 2 push with very close timestamps *)
+let mirror_action ~bot_info ?(force = true) ~owner ~repo ~base_ref ~head_sha ()
+    =
+  (let open Lwt_result.Infix in
+  let local_ref = head_sha in
+  let gh_ref =
+    {repo_url= f "https://github.com/%s/%s" owner repo; name= base_ref}
+  in
+  (* TODO: generalize to case where mapping is not one-to-one *)
+  let gl_ref =
+    { repo_url= gitlab_repo ~bot_info ~gitlab_full_name:(owner ^ "/" ^ repo)
+    ; name= base_ref }
+  in
+  git_fetch gh_ref local_ref |> execute_cmd
+  >>= fun () -> git_push ~force ~remote_ref:gl_ref ~local_ref () |> execute_cmd
+  )
+  >>= function
+  | Ok () ->
+      Lwt.return_unit
+  | Error e ->
+      Lwt_io.printlf "Error while mirroring branch %s of repository %s/%s: %s"
+        base_ref owner repo e
+
+(* TODO: ensure there's no race condition for 2 push with very close timestamps *)
 let update_pr ?full_ci ?(skip_author_check = false) ~bot_info
     (pr_info : issue_info pull_request_info) ~gitlab_mapping ~github_mapping =
   let open Lwt_result.Infix in
@@ -2599,7 +2623,7 @@ let project_action ~bot_info ~(issue : issue) ~column_id =
   | _ ->
       Lwt_io.printf "This was not a request inclusion column: ignoring.\n"
 
-let push_action ~bot_info ~base_ref ~commits_msg =
+let coq_push_action ~bot_info ~base_ref ~commits_msg =
   Stdio.printf "Merge and backport commit messages:\n" ;
   let commit_action commit_msg =
     if string_match ~regexp:"^Merge PR #\\([0-9]*\\):" commit_msg then
diff --git a/src/actions.mli b/src/actions.mli
index 37081bde..2199250c 100644
--- a/src/actions.mli
+++ b/src/actions.mli
@@ -76,12 +76,22 @@ val adjust_milestone :
 val project_action :
   bot_info:Bot_info.t -> issue:GitHub_types.issue -> column_id:int -> unit Lwt.t
 
-val push_action :
+val coq_push_action :
      bot_info:Bot_info.t
   -> base_ref:string
   -> commits_msg:string list
   -> unit Lwt.t
 
+val mirror_action :
+     bot_info:Bot_info.t
+  -> ?force:bool
+  -> owner:string
+  -> repo:string
+  -> base_ref:string
+  -> head_sha:string
+  -> unit
+  -> unit Lwt.t
+
 val ci_minimize :
      bot_info:Bot_info.t
   -> comment_info:GitHub_types.comment_info
diff --git a/src/bot.ml b/src/bot.ml
index b803aa06..2500391d 100644
--- a/src/bot.ml
+++ b/src/bot.ml
@@ -207,14 +207,38 @@ let callback _conn req body =
         GitHub_subscriptions.receive_github ~secret:github_webhook_secret
           (Request.headers req) body
       with
-      | Ok (_, PushEvent {owner; repo; base_ref; commits_msg}) ->
+      | Ok (true, PushEvent {owner= "coq"; repo= "coq"; base_ref; commits_msg})
+        ->
           (fun () ->
             init_git_bare_repository ~bot_info
             >>= fun () ->
-            action_as_github_app ~bot_info ~key ~app_id ~owner ~repo
-              (push_action ~base_ref ~commits_msg) )
+            action_as_github_app ~bot_info ~key ~app_id ~owner:"coq" ~repo:"coq"
+              (coq_push_action ~base_ref ~commits_msg) )
           |> Lwt.async ;
-          Server.respond_string ~status:`OK ~body:"Processing push event." ()
+          Server.respond_string ~status:`OK
+            ~body:
+              "Processing push event on Coq repository: analyzing merge / \
+               backporting info."
+            ()
+      | Ok (true, PushEvent {owner; repo; base_ref; head_sha; _}) -> (
+        match (owner, repo) with
+        | "coq-community", ("docker-base" | "docker-coq")
+        (*| "math-comp", ("docker-mathcomp" | "math-comp")*) ->
+            (fun () ->
+              init_git_bare_repository ~bot_info
+              >>= fun () ->
+              action_as_github_app ~bot_info ~key ~app_id ~owner ~repo
+                (mirror_action ~owner ~repo ~base_ref ~head_sha ()) )
+            |> Lwt.async ;
+            Server.respond_string ~status:`OK
+              ~body:
+                (f
+                   "Processing push event on %s/%s repository: mirroring \
+                    branch on GitLab."
+                   owner repo )
+              ()
+        | _ ->
+            Server.respond_string ~status:`OK ~body:"Ignoring push event." () )
       | Ok (_, PullRequestUpdated (PullRequestClosed, pr_info)) ->
           (fun () ->
             init_git_bare_repository ~bot_info
diff --git a/src/git_utils.ml b/src/git_utils.ml
index ace611df..f1645c57 100644
--- a/src/git_utils.ml
+++ b/src/git_utils.ml
@@ -57,7 +57,7 @@ let gitlab_ref ~bot_info ~(issue : issue) ~github_mapping ~gitlab_mapping =
   | Some r ->
       Lwt.return r )
   >|= fun gitlab_full_name ->
-  { name= f "pr-%d" issue.number
+  { name= f "refs/heads/pr-%d" issue.number
   ; repo_url= gitlab_repo ~gitlab_full_name ~bot_info }
 
 let ( |&& ) command1 command2 = command1 ^ " && " ^ command2
@@ -83,7 +83,7 @@ let git_fetch ?(force = true) remote_ref local_branch_name =
     (Stdlib.Filename.quote local_branch_name)
 
 let git_push ?(force = true) ?(options = "") ~remote_ref ~local_ref () =
-  f "git push %s %s%s:refs/heads/%s %s" remote_ref.repo_url
+  f "git push %s %s%s:%s %s" remote_ref.repo_url
     (if force then " +" else " ")
     (Stdlib.Filename.quote local_ref)
     (Stdlib.Filename.quote remote_ref.name)
diff --git a/src/git_utils.mli b/src/git_utils.mli
index 465eb1f8..e42dbb11 100644
--- a/src/git_utils.mli
+++ b/src/git_utils.mli
@@ -1,3 +1,6 @@
+val gitlab_repo :
+  bot_info:Bot_components.Bot_info.t -> gitlab_full_name:string -> string
+
 val gitlab_ref :
      bot_info:Bot_components.Bot_info.t
   -> issue:Bot_components.GitHub_types.issue