From 093485d491be3fe1f6c656dd156d97af2c1556e5 Mon Sep 17 00:00:00 2001 From: Tim van der Meij Date: Sun, 17 Nov 2024 19:24:04 +0100 Subject: [PATCH] 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. --- .gitpod.Dockerfile | 7 ------- .gitpod.yml | 13 ------------- 2 files changed, 20 deletions(-) delete mode 100644 .gitpod.Dockerfile delete mode 100644 .gitpod.yml diff --git a/.gitpod.Dockerfile b/.gitpod.Dockerfile deleted file mode 100644 index 43355323f..000000000 --- a/.gitpod.Dockerfile +++ /dev/null @@ -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/* diff --git a/.gitpod.yml b/.gitpod.yml deleted file mode 100644 index 648e81e3f..000000000 --- a/.gitpod.yml +++ /dev/null @@ -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