Fix tutorial problems per digama0#37

Fix problems noted in digama0#37 What's missing - we need to explain how to install set.mm for the tutorial, since the tutorial requires it. Signed-off-by: David A. Wheeler <[email protected]>
david-a-wheeler · May 1, 2020 · 86c25af · 86c25af
1 parent e4bfd3b
commit 86c25af
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/mmj2jar/RunParmsPATutorial.txt b/mmj2jar/RunParmsPATutorial.txt
@@ -1,9 +1,9 @@
-LoadFile,setFirst100.mm
+LoadFile,set.mm
 VerifyProof,*
 Parse,*
 ProofAsstIncompleteStepCursor,Last
 ProofAsstUnifySearchExclude,biigb,xxxid,dummylink
 ProofAsstProofFolder,PATutorial
 TheoremLoaderMMTFolder,PATutorial
-ProofAsstStartupProofWorksheet,PATutorial\Page101.mmp
+ProofAsstStartupProofWorksheet,PATutorial/Page101.mmp
 RunProofAsstGUI
diff --git a/mmj2jar/mmj2PATutorial.bat b/mmj2jar/mmj2PATutorial.bat
@@ -1 +1 @@
-java -Xincgc -Xms128M -Xmx1280M -jar mmj2.jar RunParmsPATutorial.txt Y "" "" ""
+java -Xms128M -Xmx1280M -jar mmj2.jar RunParmsPATutorial.txt Y "" "" ""
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		java -Xincgc -Xms128M -Xmx1280M -jar mmj2.jar RunParmsPATutorial.txt Y "" "" ""
		java -Xms128M -Xmx1280M -jar mmj2.jar RunParmsPATutorial.txt Y "" "" ""