util/datamanager.lua
changeset 7435 92f721226753
parent 7205 5bf0ff3882aa
child 7676 177d569307fd
--- a/util/datamanager.lua	Sun May 22 14:37:52 2016 +0200
+++ b/util/datamanager.lua	Sun May 22 14:38:07 2016 +0200
@@ -17,7 +17,9 @@
 local os_remove = os.remove;
 local os_rename = os.rename;
 local tonumber = tonumber;
+local tostring = tostring;
 local next = next;
+local type = type;
 local t_insert = table.insert;
 local t_concat = table.concat;
 local envloadfile = require"util.envload".envloadfile;