Merge branch 'master' into docs_new_theme

Author: pedrominatel

.github/scripts/on-release.sh

@@ -172,6 +172,7 @@ mkdir -p "$PKG_DIR/tools"
 # Copy all core files to the package folder
 echo "Copying files for packaging ..."
 cp -f  "$GITHUB_WORKSPACE/boards.txt"              "$PKG_DIR/"
+cp -f  "$GITHUB_WORKSPACE/package.json"            "$PKG_DIR/"
 cp -f  "$GITHUB_WORKSPACE/programmers.txt"         "$PKG_DIR/"
 cp -Rf "$GITHUB_WORKSPACE/cores"                   "$PKG_DIR/"
 cp -Rf "$GITHUB_WORKSPACE/libraries"               "$PKG_DIR/"

.github/scripts/update-version.sh

@@ -1,5 +1,9 @@
 #!/bin/bash
 
+# For reference: add tools for all boards by replacing one line in each board
+# "[board].upload.tool=esptool_py" to "[board].upload.tool=esptool_py\n[board].upload.tool.default=esptool_py\n[board].upload.tool.network=esp_ota"
+#cat boards.txt | sed "s/\([a-zA-Z0-9_\-]*\)\.upload\.tool\=esptool_py/\1\.upload\.tool\=esptool_py\\n\1\.upload\.tool\.default\=esptool_py\\n\1\.upload\.tool\.network\=esp_ota/"
+
 if [ ! $# -eq 3 ]; then
 	echo "Bad number of arguments: $#" >&2
 	echo "usage: $0 <major> <minor> <patch>" >&2