ProgTutorial/Intro.thy
changeset 486 45cfd2ece7bd
parent 485 f3536f0b47a9
child 502 615780a701b6
--- a/ProgTutorial/Intro.thy	Sat Nov 05 18:44:28 2011 +0000
+++ b/ProgTutorial/Intro.thy	Sun Nov 06 15:15:59 2011 +0000
@@ -221,36 +221,31 @@
   of many developers. Therefore, disruptions that break the work of others
   are generally frowned upon. ``Accidents'' however do happen and everybody knows
   this. Still to keep them to a minimum, you can submit your changes first to a rather 
-  sophisticated \emph{testboard}, which will perform checks of your changes agains the
+  sophisticated \emph{testboard}, which will perform checks of your changes against the
   Isabelle repository and against the AFP. The advantage of the testboard is
   that the testing is performed by rather powerful machines, saving you lengthy
-  tests on, for example, your laptop. You can see the results of the testboard 
+  tests on, for example, your own laptop. You can see the results of the testboard 
   at 
 
-  \begin{isabelle}
-  ??
-  \end{isabelle}
+  \begin{center}
+  \url{http://isabelle.in.tum.de/testboard/Isabelle/}
+  \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). To facilitate the use of the testboard you should add 
+  have to allow some time). You can summit any changes to the testboard using the 
+  command
 
-  \begin{isabelle}
-  \begin{tabular}{@ {}l}
-  @{text "[path]"}\\
-  @{text "testboard = "}
-  \end{tabular}
-  \end{isabelle}
+  @{text [display] "$ hg push -f ssh://...@macbroy21.informatik.tu-muenchen.de\\
+   //home/isabelle-repository/repos/testboard"}
 
-  to your Mercurial settings file. Then you can test any changes using the command
-
-  @{text [display] "$ hg push -f testboard"}
-
-  Note that for pushing changes to the testboard you need to add the option @{text "-f"},
-  which however 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.
+  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 @{text "-f"},
+  which however 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.
 *}