[Web] Rename JavaScript platform to Web.

Also rename export name from "HTML5" to "Web".
This commit is contained in:
Fabio Alessandrelli
2022-08-28 20:27:45 +02:00
parent 223e083d36
commit d20b32186f
120 changed files with 547 additions and 548 deletions

View File

@ -106,7 +106,7 @@ platform_arg = ARGUMENTS.get("platform", ARGUMENTS.get("p", False))
if platform_arg == "android":
custom_tools = ["clang", "clang++", "as", "ar", "link"]
elif platform_arg == "javascript":
elif platform_arg == "web":
# Use generic POSIX build toolchain for Emscripten.
custom_tools = ["cc", "c++", "ar", "link", "textfile", "zip"]
elif os.name == "nt" and methods.get_cmdline_bool("use_mingw", False):