From 43c8894e56290dae4bfb93c0361bc396664e1b1f Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 8 Sep 2011 12:32:18 +0000 Subject: [PATCH] Matitaweb: Some changes in file selection dialogbox. --- matitaB/matita/index.html | 5 +++-- matitaB/matita/matitaFilesystem.ml | 14 +++++++------- matitaB/matita/matitaweb.css | 6 ++++++ matitaB/matita/treeview/xmlTree.js | 3 ++- 4 files changed, 18 insertions(+), 10 deletions(-) diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html index 9a2343aa4..28e0ef68a 100644 --- a/matitaB/matita/index.html +++ b/matitaB/matita/index.html @@ -26,10 +26,10 @@ id="cursor" alt="Play" title="Execute the script until the current position of the cursor."> + id="bottom" alt="Bottom" title="Execute the whole script."> -