# HG changeset patch
# User wenzelm
# Date 1576767352 -3600
# Node ID 26614beb3529400b79224dd9e3b3bb80f4b34783
# Parent  1be996d8bb982416c4e177bdb3db46b87243735f
removed somewhat pointless option -R: more careful inspection of hgrc is required in practice;

diff -r 1be996d8bb98 -r 26614beb3529 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Thu Dec 19 15:29:48 2019 +0100
+++ b/src/Pure/General/mercurial.scala	Thu Dec 19 15:55:52 2019 +0100
@@ -226,7 +226,6 @@
     remote: String,
     local_path: Path,
     remote_name: String = "",
-    pull_source: String = "",
     path_name: String = default_path_name,
     progress: Progress = No_Progress)
   {
@@ -281,8 +280,6 @@
 
     progress.echo("Synchronizing ...")
 
-    if (pull_source.nonEmpty) local_hg.pull(remote = pull_source)
-
     edit_hgrc(local_hg, path_name, remote_url)
 
     local_hg.pull(options = "-u")
@@ -293,7 +290,6 @@
   val isabelle_tool =
     Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository", args =>
     {
-      var pull_source = ""
       var remote_name = ""
       var path_name = default_path_name
 
@@ -301,7 +297,6 @@
 Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL
 
   Options are:
-    -P SOURCE    pull local repository from existing source
     -n NAME      remote repository name (default: base name of LOCAL directory)
     -p PATH      Mercurial path name (default: """ + quote(default_path_name) + """)
 
@@ -309,7 +304,6 @@
   Phabricator server "user@host" or SSH file server "ssh://user@host/path".
   Both the remote and local repository are initialized on demand.
 """,
-        "P" -> (arg => pull_source = arg),
         "n:" -> (arg => remote_name = arg),
         "p:" -> (arg => path_name = arg))
 
@@ -323,7 +317,7 @@
 
       val progress = new Console_Progress
 
-      hg_setup(remote, local_path, remote_name = remote_name, pull_source = pull_source,
-        path_name = path_name, progress = progress)
+      hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name,
+        progress = progress)
     })
 }