From d20b32186fc192f5e527a1211291b0cb293f4e66 Mon Sep 17 00:00:00 2001 From: Fabio Alessandrelli Date: Sun, 28 Aug 2022 20:27:45 +0200 Subject: [Web] Rename JavaScript platform to Web. Also rename export name from "HTML5" to "Web". --- modules/mono/build_scripts/mono_configure.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'modules/mono/build_scripts') diff --git a/modules/mono/build_scripts/mono_configure.py b/modules/mono/build_scripts/mono_configure.py index ef7dbabf66..c2d5452837 100644 --- a/modules/mono/build_scripts/mono_configure.py +++ b/modules/mono/build_scripts/mono_configure.py @@ -16,7 +16,7 @@ def module_supports_tools_on(platform): def configure(env, env_mono): # is_android = env["platform"] == "android" - # is_javascript = env["platform"] == "javascript" + # is_web = env["platform"] == "web" # is_ios = env["platform"] == "ios" # is_ios_sim = is_ios and env["arch"] in ["x86_32", "x86_64"] -- cgit v1.2.3