updated testboard section default tip
authorChristian Urban <urbanc@in.tum.de>
Sun, 16 Jun 2019 14:54:32 +0100
changeset 580 883ce9c7b13b
parent 579 4dc20f6921d0
updated testboard section
ProgTutorial/Intro.thy
progtutorial.pdf
--- a/ProgTutorial/Intro.thy	Tue Jun 11 23:31:53 2019 +0100
+++ b/ProgTutorial/Intro.thy	Sun Jun 16 14:54:32 2019 +0100
@@ -288,25 +288,27 @@
   at 
 
   \begin{center}
-  \url{http://isabelle.in.tum.de/testboard/Isabelle/}
+  \url{https://ci.isabelle.systems/status}
   \end{center}
 
-  which is organised like a Mercurial repository. A green point next to a change
-  indicates that the change passes the corresponding tests (for this of course you
-  have to allow some time). You can summit any changes to the testboard using the 
+  You can summit any changes to the Isabelle testboard using the 
   command
 
-  @{text [display] "$ hg push -f ssh://...@hgbroy.informatik.tu-muenchen.de\\
-   //home/isabelle-repository/repos/testboard"}
+  @{text [display] "$ hg push -f ssh://...@isabelle-server.in.tum.de//home/isabelle-repository\\  
+  /repos/testboard"}
+
+  and to the AFP testboard
+
+  @{text [display] "$ hg push -f ssh://hg@bitbucket.org/isa-afp/afp-testboard"}
 
-  where the dots need to be replaced by your login name.  Note that for
-  pushing changes to the testboard you need to add the option \<open>-f\<close>,
-  which should \emph{never} be used with the main Isabelle
-  repository. While the testboard is a great system for supporting Isabelle
-  developers, its disadvantage is that it needs login permissions for the
-  computers in Munich. So in order to use it, you might have to ask other
-  developers to obtain one.
-\<close>
+  where the dots in the first command need to be replaced by your
+  login name.  Note that for pushing changes to the testboard you need
+  to add the option \<open>-f\<close>, which should \emph{never} be
+  used with the main Isabelle repository. While the testboard is a
+  great system for supporting Isabelle developers, its disadvantage is
+  that it needs login permissions for the computers in Munich. So in
+  order to use it, you might have to ask other developers to obtain
+  one.  \<close>
 
 
 section \<open>Some Naming Conventions in the Isabelle Sources\<close>
Binary file progtutorial.pdf has changed