2021-07-31 20:49:32 +02:00
|
|
|
#!/usr/bin/env bash
|
2019-07-03 15:52:03 +02:00
|
|
|
#
|
|
|
|
# This script assumes a linux environment
|
|
|
|
|
2021-07-31 23:34:25 +02:00
|
|
|
set -e
|
|
|
|
|
2019-07-03 15:52:03 +02:00
|
|
|
DES=$1
|
|
|
|
|
|
|
|
bash ./tools/make-assets.sh $DES
|
|
|
|
|
|
|
|
cp -R src/css $DES/
|
|
|
|
cp -R src/img $DES/
|
2021-07-25 16:55:35 +02:00
|
|
|
mkdir $DES/js
|
|
|
|
cp -R src/js/*.js $DES/js/
|
|
|
|
cp -R src/js/codemirror $DES/js/
|
|
|
|
cp -R src/js/scriptlets $DES/js/
|
|
|
|
cp -R src/js/wasm $DES/js/
|
2019-07-03 15:52:03 +02:00
|
|
|
cp -R src/lib $DES/
|
|
|
|
cp -R src/web_accessible_resources $DES/
|
|
|
|
cp -R src/_locales $DES/
|
|
|
|
|
|
|
|
cp src/*.html $DES/
|
2021-07-16 16:06:58 +02:00
|
|
|
cp platform/common/*.js $DES/js/
|
|
|
|
cp platform/common/*.json $DES/
|
2019-07-03 15:52:03 +02:00
|
|
|
cp LICENSE.txt $DES/
|