Remove obsolete Gitpod files

In PR #11300 Gitpod support got introduced, but we re-evaluated that
decision in #11732. In PR #11800 the support was partially reverted,
but the actual Gitpod files were kept to not outright break potential
workflows because at the time we were not sure if, and if so how often,
Gitpod was actually used for contributing to PDF.js.

However, in addition to the concerns mentioned in #11732 after five
years we haven't seen any contributions that clearly originated from
Gitpod, and the files have not been updated after e.g. PR #11807 and
PR #17913 because it's not a workflow that we maintain or are able
to test (nor have we seen Gitpod community contributions for this).

This commit therefore removes the remaining Gitpod files to reduce
maintainance burden for PDF.js. Note that users of Gitpod can still
contribute to PDF.js via the platform; we just don't provide/manage
workspace files from this repository anymore.
This commit is contained in:
Tim van der Meij 2024-11-17 19:24:04 +01:00
parent 8a8b69f456
commit 093485d491
No known key found for this signature in database
GPG Key ID: 8C3FD2925A5F2762
2 changed files with 0 additions and 20 deletions

7
.gitpod.Dockerfile vendored
View File

@ -1,7 +0,0 @@
FROM gitpod/workspace-full-vnc
USER gitpod
RUN sudo apt-get update && \
sudo apt-get install -yq firefox && \
sudo rm -rf /var/lib/apt/lists/*

View File

@ -1,13 +0,0 @@
image:
file: .gitpod.Dockerfile
tasks:
- command: |
gp await-port 8888 && gp preview $(gp url 8888)/web/viewer.html && echo '[{"name": "Firefox","path": "/usr/bin/firefox"}]' | jq '.' > test/resources/browser_manifests/browser_manifest.json
- init: npm install -g gulp-cli && npm install
command: gulp server
ports:
- port: 8888
onOpen: ignore
- port: 6080
onOpen: ignore