From 8c78f4d17778d4c83c7159b0d74803886b8f01a7 Mon Sep 17 00:00:00 2001
From: charguer <arthur@chargueraud.org>
Date: Fri, 25 Mar 2016 09:40:20 +0100
Subject: [PATCH] cleanup_deprecated
---
.../convert-ml-strings.pl | 0
demo_trace.js => deprecated/demo_trace.js | 0
interp-poc.js => deprecated/interp-poc.js | 0
interp.js => deprecated/interp.js | 0
.../ml-add-cstr-annots.pl | 0
navig-poc.html => deprecated/navig-poc.html | 0
navig-poc.js => deprecated/navig-poc.js | 0
navig.html => deprecated/navig.html | 0
navig.js => deprecated/navig.js | 0
source-driver.js => deprecated/source-driver.js | 0
source-poc.js => deprecated/source-poc.js | 0
test.html => deprecated/test.html | 0
driver.html | 11 +++++++++++
13 files changed, 11 insertions(+)
rename convert-ml-strings.pl => deprecated/convert-ml-strings.pl (100%)
rename demo_trace.js => deprecated/demo_trace.js (100%)
rename interp-poc.js => deprecated/interp-poc.js (100%)
rename interp.js => deprecated/interp.js (100%)
rename ml-add-cstr-annots.pl => deprecated/ml-add-cstr-annots.pl (100%)
rename navig-poc.html => deprecated/navig-poc.html (100%)
rename navig-poc.js => deprecated/navig-poc.js (100%)
rename navig.html => deprecated/navig.html (100%)
rename navig.js => deprecated/navig.js (100%)
rename source-driver.js => deprecated/source-driver.js (100%)
rename source-poc.js => deprecated/source-poc.js (100%)
rename test.html => deprecated/test.html (100%)
diff --git a/convert-ml-strings.pl b/deprecated/convert-ml-strings.pl
similarity index 100%
rename from convert-ml-strings.pl
rename to deprecated/convert-ml-strings.pl
diff --git a/demo_trace.js b/deprecated/demo_trace.js
similarity index 100%
rename from demo_trace.js
rename to deprecated/demo_trace.js
diff --git a/interp-poc.js b/deprecated/interp-poc.js
similarity index 100%
rename from interp-poc.js
rename to deprecated/interp-poc.js
diff --git a/interp.js b/deprecated/interp.js
similarity index 100%
rename from interp.js
rename to deprecated/interp.js
diff --git a/ml-add-cstr-annots.pl b/deprecated/ml-add-cstr-annots.pl
similarity index 100%
rename from ml-add-cstr-annots.pl
rename to deprecated/ml-add-cstr-annots.pl
diff --git a/navig-poc.html b/deprecated/navig-poc.html
similarity index 100%
rename from navig-poc.html
rename to deprecated/navig-poc.html
diff --git a/navig-poc.js b/deprecated/navig-poc.js
similarity index 100%
rename from navig-poc.js
rename to deprecated/navig-poc.js
diff --git a/navig.html b/deprecated/navig.html
similarity index 100%
rename from navig.html
rename to deprecated/navig.html
diff --git a/navig.js b/deprecated/navig.js
similarity index 100%
rename from navig.js
rename to deprecated/navig.js
diff --git a/source-driver.js b/deprecated/source-driver.js
similarity index 100%
rename from source-driver.js
rename to deprecated/source-driver.js
diff --git a/source-poc.js b/deprecated/source-poc.js
similarity index 100%
rename from source-poc.js
rename to deprecated/source-poc.js
diff --git a/test.html b/deprecated/test.html
similarity index 100%
rename from test.html
rename to deprecated/test.html
diff --git a/driver.html b/driver.html
index 94ef79c..f459dd4 100644
--- a/driver.html
+++ b/driver.html
@@ -183,3 +183,14 @@ $(function() {
+
+
+
+<!---
+
+var t = []; for (var i = 0; i < 3; i++) { t[i] = function() { return i; } };
+() { return i; }
+t[0]();
+3
+
+-->
\ No newline at end of file
--
GitLab