From: Wilmer Ricciotti
Date: Wed, 22 Jun 2011 15:32:03 +0000 (+0000)
Subject: Removed filename input box from index.html (just browse the library now).
X-Git-Tag: make_still_working~2397
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=89d112fde68f8b6268912f21da2c29f12cac5a39;p=helm.git
Removed filename input box from index.html (just browse the library now).
---
diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html
index ab46665d3..7fa3b88ac 100644
--- a/matitaB/matita/index.html
+++ b/matitaB/matita/index.html
@@ -26,8 +26,7 @@
title="Execute the script until the current position of the cursor.">
-