From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 19 Sep 2003 12:44:51 +0000 (+0000)
Subject: Clean cache method added.
X-Git-Tag: V_0_4_3_4~23
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b25d974b6feb403cb551e0cb9776267f2d46ce7e;p=helm.git

Clean cache method added.
---

diff --git a/helm/http_getter/panel/control.html b/helm/http_getter/panel/control.html
index 60c60ebed..47f2c14ac 100644
--- a/helm/http_getter/panel/control.html
+++ b/helm/http_getter/panel/control.html
@@ -69,6 +69,14 @@ If you have troubles, please send an email to the author:
       </form>
     </td>
   </tr>
+  <tr>
+    <td>
+      <form>
+        <b>Clean cache</b> (must be done every time a file is modified)<br />
+        <input type="button" value="Clean" onClick="top.result.location.replace(getGetterURL() + 'cleancache')"/>
+      </form>
+    </td>
+  </tr>
   <tr>
     <td>
       <form>