]> matita.cs.unibo.it Git - helm.git/commitdiff
library3 ==> javascript
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Mar 2001 16:10:16 +0000 (16:10 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Mar 2001 16:10:16 +0000 (16:10 +0000)
helm/cgi/mkcontrol.pl
helm/cgi/mkheader.pl
helm/cgi/mkindexcic.pl
helm/cgi/mkindextheory.pl

index 6e593d7d8d840b2a06906a29eaa06f26b2b15e16..96c5c952274d3f9862a15bc9a300d14a807c78bc 100755 (executable)
@@ -38,7 +38,7 @@ Content-type: text/html
 <html>
 <head>
 <title>Control panel</title>
-<script language="JavaScript" src="http://phd.cs.unibo.it/helm/library3/control.js">
+<script language="JavaScript" src="http://phd.cs.unibo.it/helm/javascript/control.js">
 </script>
 </head>
 <body bgcolor="#ffffff" text="#000000">
index a8e99754f5b1ff52af90f1b381746c96723210bc..b3db1cfa33d9708d22a93d91ddada5bb9f5006a8 100755 (executable)
@@ -27,7 +27,7 @@ Content-type: text/html
 <html>
 <head>
 <title>Control panel</title>
-<script language="JavaScript" src="http://phd.cs.unibo.it/helm/library3/control.js">
+<script language="JavaScript" src="http://phd.cs.unibo.it/helm/javascript/control.js">
 </script>
 </head>
 <body bgcolor="#ffffff" text="#000000">
index 6f816d3271a660d4d28348ce8eae36cd5ffbf530..0033a512ae210a7ec954e1f9f4478958df1f3b3f 100755 (executable)
@@ -98,7 +98,7 @@ Content-type: text/html
 <html>
 <head>
 <title>Index of $uri</title>
-<script language="JavaScript" src="http://phd.cs.unibo.it/helm/library3/control.js">
+<script language="JavaScript" src="http://phd.cs.unibo.it/helm/javascript/control.js">
 </script>
 </head>
 <body bgcolor="#ffffff" text="#000000">
index fc203ff0fa154f4bdcdca0fc2f7d2b6e7a345455..05bb5b925bf91fbc48255c9c25b0ef4afe79373b 100755 (executable)
@@ -87,7 +87,7 @@ Content-type: text/html
 <html>
 <head>
 <title>Index of $uri</title>
-<script language="JavaScript" src="http://phd.cs.unibo.it/helm/library3/control.js">
+<script language="JavaScript" src="http://phd.cs.unibo.it/helm/javascript/control.js">
 </script>
 </head>
 <body bgcolor="#ffffff" text="#000000">