diff --git a/.gitignore b/.gitignore index 01e4bed1..3b505524 100644 --- a/.gitignore +++ b/.gitignore @@ -37,5 +37,6 @@ c_mpos/breakout/build # build files *.bin -# auto created by inline_minify_webrepl.py -internal_filesystem/builtin/html/webrepl_inlined_minified.html +# auto created by inline_minify_webrepl.py but still checked in because it's a small file +# and when users download internal_filesystem/ from git (to run a statically compiled Linux build, for example) they need this +# internal_filesystem/builtin/html/webrepl_inlined_minified.html diff --git a/internal_filesystem/builtin/html/README.md b/internal_filesystem/builtin/html/README.md index ddacaedb..d95ffd72 100644 --- a/internal_filesystem/builtin/html/README.md +++ b/internal_filesystem/builtin/html/README.md @@ -1 +1 @@ -This folder will be filled by the inline_minify_webrepl.py script. +This folder gets filled by the webrepl/inline_minify_webrepl.py script. diff --git a/internal_filesystem/builtin/html/webrepl_inlined_minified.html b/internal_filesystem/builtin/html/webrepl_inlined_minified.html new file mode 100644 index 00000000..6ef57225 --- /dev/null +++ b/internal_filesystem/builtin/html/webrepl_inlined_minified.html @@ -0,0 +1,48 @@ + + +
+