Learn how easy it is to sync an existing GitHub or Google Code repo to a SourceForge project! See Demo


Diff of /doc/editors/new-entry-checkin.html [a2ca86] .. [1e911d] Maximize Restore

  Switch to side-by-side view

--- a/doc/editors/new-entry-checkin.html
+++ b/doc/editors/new-entry-checkin.html
@@ -75,7 +75,7 @@
 category, add it to metadata/topics (make sure there is an empty line at the
 end of the file). </li>
-<li>Generate the new web site by running <code>../admin/sitegen</code>.</li>
+<li>Generate the new web site by running <code>../admin/sitegen</code> .</li>
 <li>Use <code>hg st</code> and <code>hg diff</code> to make sure the generated html makes sense. The diff should be small and concern the new entry only.</li>
@@ -85,7 +85,7 @@
 <li>to publish the changes to the web, run<br>
-cd ~/afp/release/admin<br>
+cd ../admin<br>
 ./publish -r Isabelle201X &lt;name&gt;