]> matita.cs.unibo.it Git - helm.git/commitdiff
Clean cache method added.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 19 Sep 2003 12:44:51 +0000 (12:44 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 19 Sep 2003 12:44:51 +0000 (12:44 +0000)
helm/http_getter/panel/control.html

index 60c60ebedf441d0614c3617c0e046f6193959bd7..47f2c14ac467d41ef0aed31f5965961f6f54d405 100644 (file)
@@ -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>