webext: fix options_ui.js removal + remove unused options_ui.html

per ec3d1bfc88
7 years ago · a36042b5ce
2 changed files with 1 additions and 15 deletions
--- a/platform/webext/options_ui.html
+++ b/platform/webext/options_ui.html
@ -1,12 +0,0 @@
 <!DOCTYPE html>
 <head>
 <meta charset="utf-8">
 <title></title>
 </head>
 <body>
 <a href="dashboard.html" data-i18n="matrixDashboardMenuEntry" target="uMatrix-dashboard"></a><br>
 <a href="logger-ui.html" data-i18n="matrixLoggerMenuEntry" target="uMatrix-logger"></a>
 </body>
 <script src="js/vapi-common.js"></script>
 <script src="js/i18n.js"></script>
 </html>
--- a/tools/make-webext.sh
+++ b/tools/make-webext.sh
@ -16,15 +16,13 @@ cp    platform/chromium/*.js               $DES/js/
 cp -R platform/chromium/img/*              $DES/img/
 cp    LICENSE.txt                          $DES/
 cp    platform/webext/options_ui.html      $DES/
 rm    $DES/js/options_ui.js
 cp    platform/webext/polyfill.js          $DES/js/
 cp    platform/webext/vapi-cachestorage.js $DES/js/
 cp    platform/webext/manifest.json        $DES/
 # webext-specific
 rm $DES/options_ui.html
 rm $DES/options_ui.js
 rm $DES/js/options_ui.js
 echo "*** uMatrix.webext: Generating meta..."
 python tools/make-webext-meta.py           $DES/