From 9ca6b45a45f1cc4cb30a4f36f9939dbedf657e6e Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 4 Sep 2003 16:45:25 +0000
Subject: [PATCH] commented out debugging tutor "wait"

---
 helm/hbugs/tutors/INDEX.xml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/helm/hbugs/tutors/INDEX.xml b/helm/hbugs/tutors/INDEX.xml
index 9de351709..7936066b2 100644
--- a/helm/hbugs/tutors/INDEX.xml
+++ b/helm/hbugs/tutors/INDEX.xml
@@ -21,6 +21,19 @@
 -->
 
 <tutors>
+
+  <!-- DEBUGGING -->
+<!--
+  <tutor source="wait_tutor.ml">
+    <addr>127.0.0.1</addr>
+    <port>50111</port>
+    <tactic>Wait.wait_tac</tactic>
+    <hint>Hbugs_types.Use_ring_Luke</hint>
+    <hint_type>Use Ring Luke</hint_type>
+    <description>WAIT FOREVER tutor</description>
+  </tutor>
+-->
+
   <tutor source="ring_tutor.ml">
     <addr>127.0.0.1</addr>
     <port>50001</port>
-- 
2.39.2