jeans/arduino-ide
1
0
Fork 0
mirror of https://github.com/arduino/arduino-ide.git synced 2025-11-09 02:18:32 +00:00
Code Issues Packages Projects Releases Wiki Activity

Updated Theia to 1.25.0

Browse Source 
Co-authored-by: Mark Sujew <mark.sujew@typefox.io>
Co-authored-by: Akos Kitta <a.kitta@arduino.cc>

Signed-off-by: Akos Kitta <a.kitta@arduino.cc>
This commit is contained in:
Mark Sujew
2022-03-08 14:59:30 +01:00
committed by Akos Kitta
parent b8c718ce9e
commit 1ae60ec9bc
202 changed files with 4461 additions and 3602 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
electron/build/scripts/patch-theia-preload.js Normal file
View File

@@ -0,0 +1,16 @@
// Patch the Theia spinner: https://github.com/eclipse-theia/theia/pull/10761#issuecomment-1131476318
// Replaces the `theia-preload` selector with `old-theia-preload` in the generated `index.html`.
let arg = process.argv.splice(2)[0]
if (!arg) {
console.error("The path to the index.html to patch is missing. Use 'node patch-theia-preload.js ./path/to/index.html'")
process.exit(1)
}
(async () => {
const { promises: fs } = require('fs')
const path = require('path')
const index = path.isAbsolute(arg) ? arg : path.join(process.cwd(), arg)
console.log(`>>> Patching 'theia-preload' with 'old-theia-preload' in ${index}.`)
const content = await fs.readFile(index, { encoding: 'utf-8' })
await fs.writeFile(index, content.replace(/theia-preload/g, 'old-theia-preload'), { encoding: 'utf-8' })
console.log(`<<< Successfully patched index.html.`)
})()