build: enable GitPod prebuilds

PR-URL: #43698
Reviewed-By: Matteo Collina <[email protected]>
Reviewed-By: Antoine du Hamel <[email protected]>
Reviewed-By: Michael Dawson <[email protected]>
Reviewed-By: Franziska Hinkelmann <[email protected]>
Reviewed-By: Michaël Zasso <[email protected]>
Reviewed-By: Danielle Adams <[email protected]>
Reviewed-By: Darshan Sen <[email protected]>

Author: Trott

.gitignore

@@ -19,6 +19,7 @@
 !.github
 !.gitignore
 !.gitkeep
+!.gitpod.yml
 !.mailmap
 !.nycrc
 !.yamllint.yaml

.gitpod.yml

@@ -0,0 +1,9 @@
+# Ref: https://github.com/gitpod-io/gitpod/issues/6283#issuecomment-1001043454
+tasks:
+  - init: ./configure && timeout 50m make -j16 || true
+
+# Ref: https://www.gitpod.io/docs/prebuilds#github-specific-configuration
+github:
+  prebuilds:
+    # add a "Review in Gitpod" button as a comment to pull requests (defaults to true)
+    addComment: false