Matitaweb:

[helm.git] / matitaB / matita / index.html
diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html

index 067189d7382f1418ee04a1031b39b6f11660e1b5..21ffb0e5c00b486021cee339510970f7b825f4ea 100644 (file)
--- a/matitaB/matita/index.html
+++ b/matitaB/matita/index.html
@@ -2,17 +2,19 @@
  
  <head>
  <script type="text/javascript" src="jquery.js"></script>
+<script type="text/javascript" src="jquery.tooltip.min.js"></script>
  <script type="text/javascript" src="utf8MacroTable.js"></script>
  <script type="text/javascript" src="matitaweb.js"></script>
  <script type="text/javascript" src="layout.js"></script>
  <link rel="stylesheet" type="text/css" href="matitaweb.css"/>
+<link rel="stylesheet" type="text/css" href="jquery.tooltip.css"/>
  
  <link href="treeview/xmlTree.css" type="text/css" rel="stylesheet"/>
  <script src="treeview/xmlTree.js" type="text/javascript"></script>
  
  </head>
  
-<body onLoad="initialize();" onResize="resize();">
+<body onLoad="initialize();">
  <textarea id="unescape" style="display:none;"></textarea>
  <div id="sandbox" style="display:none;"></div>