minor editor improvements for "paste" #190

	name: CD

	on:
	push:
	branches: [master]

	jobs:
	build-and-deploy:
	runs-on: ubuntu-latest

	steps:
	- uses: actions/checkout@v2
	with:
	persist-credentials: false
	fetch-depth: 0

	# Set up environment
	- name: Use Node.js 16.x
	uses: actions/setup-node@v1
	with:
	node-version: 16.x
	- name: Set up NPM cache
	uses: actions/cache@v2
	with:
	path: ~/.npm
	key: npm-${{ hashFiles('**/package-lock.json') }}
	restore-keys: \|
	npm-
	- name: Install dependencies
	run: npm ci

	# Build and run tests
	- name: Build IDE
	run: npm run build
	- name: Build interop
	run: npm run interop
	- name: Run tests
	run: npm test

	# Deploy to GitHub Pages
	- name: Prepare deployment
	run: \|
	rm ./out/tscript.js
	mkdir ./out/distribution
	mv ./src/ide/redirect.html ./out/distribution/index.html
	- name: Deploy to GitHub Pages
	uses: JamesIves/[email protected]
	with:
	branch: gh-pages
	folder: ./out
	single-commit: true
	git-config-name: github-actions[bot]
	git-config-email: 41898282+github-actions[bot]@users.noreply.github.com

Provide feedback