From 3849ef3e1de93cdf691e3d3ccfe32f5c243ba5e2 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 12 Oct 2023 14:31:26 +0100 Subject: [PATCH 01/18] [ ci ] new www deploy strategy --- .github/workflows/ci-ubuntu.yml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index ebafe70fa8..e250641724 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -75,7 +75,7 @@ jobs: || '${{ github.base_ref }}' == 'master' ]]; then # Pick Agda version for master echo "AGDA_COMMIT=tags/v2.6.4" >> $GITHUB_ENV; - echo "AGDA_HTML_DIR=html" >> $GITHUB_ENV + echo "AGDA_HTML_DIR=html/master" >> $GITHUB_ENV elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \ || '${{ github.base_ref }}' == 'experimental' ]]; then # Pick Agda version for experimental @@ -177,9 +177,16 @@ jobs: rm -f '${{ env.AGDA_HTML_DIR }}'/*.css ${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda + + rm html/index.html + find html/ -name "index.html" \ + | grep -v "master\|experimental" \ + | sed 's|html/\([^\/]*\)/index.html|\1|g' + >> html/index.html + - name: Deploy HTML uses: JamesIves/github-pages-deploy-action@4.1.3 - if: ${{ success() && env.AGDA_DEPLOY }} + # if: ${{ success() && env.AGDA_DEPLOY }} with: branch: gh-pages From 13999a7074f08b6df71a1ddde4a2fdc20f5e8fd7 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 12 Oct 2023 15:44:41 +0100 Subject: [PATCH 02/18] [ fix ] index.html page --- .github/workflows/ci-ubuntu.yml | 38 +++++++++++++++++++-------------- 1 file changed, 22 insertions(+), 16 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index e250641724..3c0128a125 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -144,22 +144,22 @@ jobs: ## TESTING ######################################################################## - # By default github actions do not pull the repo - - name: Checkout stdlib - uses: actions/checkout@v2 + # # By default github actions do not pull the repo + # - name: Checkout stdlib + # uses: actions/checkout@v2 - - name: Test stdlib - run: | - cabal run GenerateEverything - cp travis/* . - ./index.sh - ${{ env.AGDA }} --safe EverythingSafe.agda - ${{ env.AGDA }} index.agda + # - name: Test stdlib + # run: | + # cabal run GenerateEverything + # cp travis/* . + # ./index.sh + # ${{ env.AGDA }} --safe EverythingSafe.agda + # ${{ env.AGDA }} index.agda - - name: Golden testing - run: | - ${{ env.CABAL_INSTALL }} clock - make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' + # - name: Golden testing + # run: | + # ${{ env.CABAL_INSTALL }} clock + # make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' ######################################################################## @@ -179,10 +179,16 @@ jobs: rm html/index.html + + echo "

Development versions

" >> html/index.html + echo "master" >> html/index.html + echo "experimental" >> html/index.html + echo "

Released versions

" >> html/index.html + find html/ -name "index.html" \ | grep -v "master\|experimental" \ - | sed 's|html/\([^\/]*\)/index.html|\1|g' - >> html/index.html + | sed 's|html/\([^\/]*\)/index.html|\1|g' \ + >> html/index.html - name: Deploy HTML uses: JamesIves/github-pages-deploy-action@4.1.3 From c2b75b12f382ec6a480c43452240c47d093978fe Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 12 Oct 2023 15:59:39 +0100 Subject: [PATCH 03/18] [ fix ] reinstate index.agda generation --- .github/workflows/ci-ubuntu.yml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 3c0128a125..322f2c7b7e 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -148,11 +148,11 @@ jobs: # - name: Checkout stdlib # uses: actions/checkout@v2 - # - name: Test stdlib - # run: | - # cabal run GenerateEverything - # cp travis/* . - # ./index.sh + - name: Test stdlib + run: | + cabal run GenerateEverything + cp travis/* . + ./index.sh # ${{ env.AGDA }} --safe EverythingSafe.agda # ${{ env.AGDA }} index.agda From 9bc74fa24a69d8a9733d054ee173d797fa5d638a Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 12 Oct 2023 16:03:27 +0100 Subject: [PATCH 04/18] [ fix ] more silly mistakes --- .github/workflows/ci-ubuntu.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 322f2c7b7e..7fe5d4068d 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -144,9 +144,9 @@ jobs: ## TESTING ######################################################################## - # # By default github actions do not pull the repo - # - name: Checkout stdlib - # uses: actions/checkout@v2 + # By default github actions do not pull the repo + - name: Checkout stdlib + uses: actions/checkout@v2 - name: Test stdlib run: | From 475739f562fbbe159a1522a130bce01ebf18eb0c Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 12 Oct 2023 16:25:56 +0100 Subject: [PATCH 05/18] [ html ] more structure --- .github/workflows/ci-ubuntu.yml | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 7fe5d4068d..a0c9c4b658 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -125,6 +125,7 @@ jobs: run: cabal update - name: Install alex & happy + if: steps.cache-cabal.outputs.cache-hit != 'true' run: | ${{ env.CABAL_INSTALL }} alex ${{ env.CABAL_INSTALL }} happy @@ -178,17 +179,23 @@ jobs: ${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda - rm html/index.html - - echo "

Development versions

" >> html/index.html - echo "master" >> html/index.html - echo "experimental" >> html/index.html - echo "

Released versions

" >> html/index.html + echo "

Development versions

" >> index.html + echo "
    " >> index.html + echo "
  • master
    • " >> index.html + echo "
  • experimental
    • " >> index.html + echo "
" >> index.html + echo "

Released versions

" >> index.html + echo "
    " >> index.html find html/ -name "index.html" \ | grep -v "master\|experimental" \ - | sed 's|html/\([^\/]*\)/index.html|\1|g' \ - >> html/index.html + | sort + | sed 's|html/\([^\/]*\)/index.html|
  • \1
    • |g' \ + >> index.html + + echo "
" + + mv index.html html/ - name: Deploy HTML uses: JamesIves/github-pages-deploy-action@4.1.3 From a534f6a40044382fde80ea069fce9a5b8d477d41 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 12 Oct 2023 16:33:40 +0100 Subject: [PATCH 06/18] [ refactor ] use template file + .sh script --- .github/workflows/ci-ubuntu.yml | 20 ++------------------ travis/landing.html | 12 ++++++++++++ travis/landing.sh | 12 ++++++++++++ 3 files changed, 26 insertions(+), 18 deletions(-) create mode 100644 travis/landing.html create mode 100644 travis/landing.sh diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index a0c9c4b658..d8fa5850fe 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -178,24 +178,8 @@ jobs: rm -f '${{ env.AGDA_HTML_DIR }}'/*.css ${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda - - echo "

Development versions

" >> index.html - echo "
    " >> index.html - echo "
  • master
    • " >> index.html - echo "
  • experimental
    • " >> index.html - echo "
" >> index.html - echo "

Released versions

" >> index.html - echo "
    " >> index.html - - find html/ -name "index.html" \ - | grep -v "master\|experimental" \ - | sort - | sed 's|html/\([^\/]*\)/index.html|
  • \1
    • |g' \ - >> index.html - - echo "
" - - mv index.html html/ + cp travis/* . + ./landing.sh - name: Deploy HTML uses: JamesIves/github-pages-deploy-action@4.1.3 diff --git a/travis/landing.html b/travis/landing.html new file mode 100644 index 0000000000..c604f19ce0 --- /dev/null +++ b/travis/landing.html @@ -0,0 +1,12 @@ + + +

Development versions

+ + + +

Released versions

+ +
    diff --git a/travis/landing.sh b/travis/landing.sh new file mode 100644 index 0000000000..4cd65958a1 --- /dev/null +++ b/travis/landing.sh @@ -0,0 +1,12 @@ +set -eu +set -o pipefail + +find html/ -name "index.html" \ + | grep -v "master\|experimental" \ + | sort + | sed 's|html/\([^\/]*\)/index.html|
  • \1
    • |g' \ + >> landing.html + +echo "
" >> landing.html + +mv landing.html html/index.html From e11ab71ddf651f1f48c6f0c9a9a3a965032aefea Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 12 Oct 2023 16:36:12 +0100 Subject: [PATCH 07/18] [ fix ] no need to escape quotes in .html file --- travis/landing.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/travis/landing.html b/travis/landing.html index c604f19ce0..de84a7d580 100644 --- a/travis/landing.html +++ b/travis/landing.html @@ -3,8 +3,8 @@

Development versions

Released versions

From 00e877f3bc7fd980658b482d5cc5043428199744 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 12 Oct 2023 16:43:21 +0100 Subject: [PATCH 08/18] [ fix ] missing newline --- travis/landing.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/travis/landing.sh b/travis/landing.sh index 4cd65958a1..5c6ecde7a3 100644 --- a/travis/landing.sh +++ b/travis/landing.sh @@ -3,7 +3,7 @@ set -o pipefail find html/ -name "index.html" \ | grep -v "master\|experimental" \ - | sort + | sort \ | sed 's|html/\([^\/]*\)/index.html|
  • \1
    • |g' \ >> landing.html From e67bb8a71130f12bf3913d7c310f502f00c506b1 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 12 Oct 2023 17:02:48 +0100 Subject: [PATCH 09/18] [ fix ] make landing.sh executable --- travis/landing.sh | 0 1 file changed, 0 insertions(+), 0 deletions(-) mode change 100644 => 100755 travis/landing.sh diff --git a/travis/landing.sh b/travis/landing.sh old mode 100644 new mode 100755 From 393ede72a1ba064c728b697737ee3e77a8ae327b Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 12 Oct 2023 17:21:17 +0100 Subject: [PATCH 10/18] [ fix ] should be ready --- travis/landing.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/travis/landing.sh b/travis/landing.sh index 5c6ecde7a3..c29d23f4cd 100755 --- a/travis/landing.sh +++ b/travis/landing.sh @@ -1,6 +1,8 @@ set -eu set -o pipefail +rm html/index.html + find html/ -name "index.html" \ | grep -v "master\|experimental" \ | sort \ From 2d0afd7ccb681af6444cd7e5f63feb86c2fe6be1 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 13 Oct 2023 10:53:58 +0100 Subject: [PATCH 11/18] [ fix ] reverse order sort --- travis/landing.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/travis/landing.sh b/travis/landing.sh index c29d23f4cd..b14f9cc43c 100755 --- a/travis/landing.sh +++ b/travis/landing.sh @@ -5,7 +5,7 @@ rm html/index.html find html/ -name "index.html" \ | grep -v "master\|experimental" \ - | sort \ + | sort -r \ | sed 's|html/\([^\/]*\)/index.html|
  • \1
    • |g' \ >> landing.html From 1a942bfc06a4780f538eeccf8474e026f20eaaba Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 13 Oct 2023 10:59:13 +0100 Subject: [PATCH 12/18] [ cleanup ] More html structure --- travis/landing-bottom.html | 4 ++++ travis/landing-top.html | 19 +++++++++++++++++++ travis/landing.html | 12 ------------ travis/landing.sh | 4 +++- 4 files changed, 26 insertions(+), 13 deletions(-) create mode 100644 travis/landing-bottom.html create mode 100644 travis/landing-top.html delete mode 100644 travis/landing.html diff --git a/travis/landing-bottom.html b/travis/landing-bottom.html new file mode 100644 index 0000000000..9cd52d7c69 --- /dev/null +++ b/travis/landing-bottom.html @@ -0,0 +1,4 @@ + + + + diff --git a/travis/landing-top.html b/travis/landing-top.html new file mode 100644 index 0000000000..0d214f58b5 --- /dev/null +++ b/travis/landing-top.html @@ -0,0 +1,19 @@ + + + + Documention for the Agda standard library + + + +
    + +

    Development versions

    + + + +

    Released versions

    + +
      diff --git a/travis/landing.html b/travis/landing.html deleted file mode 100644 index de84a7d580..0000000000 --- a/travis/landing.html +++ /dev/null @@ -1,12 +0,0 @@ - - -

      Development versions

      - - - -

      Released versions

      - -
        diff --git a/travis/landing.sh b/travis/landing.sh index b14f9cc43c..d3957f558e 100755 --- a/travis/landing.sh +++ b/travis/landing.sh @@ -3,12 +3,14 @@ set -o pipefail rm html/index.html +cat landing-top.html >> landing.html + find html/ -name "index.html" \ | grep -v "master\|experimental" \ | sort -r \ | sed 's|html/\([^\/]*\)/index.html|
      • \1
        • |g' \ >> landing.html -echo "
      " >> landing.html +cat landing-bottom.html >> landing.html mv landing.html html/index.html From dcc5bb32669a3aa38b7fd39a912b41d748c8b573 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 13 Oct 2023 11:12:17 +0100 Subject: [PATCH 13/18] [ revert ] go back to building everything --- .github/workflows/ci-ubuntu.yml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index d8fa5850fe..2ecc969589 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -154,13 +154,13 @@ jobs: cabal run GenerateEverything cp travis/* . ./index.sh - # ${{ env.AGDA }} --safe EverythingSafe.agda - # ${{ env.AGDA }} index.agda + ${{ env.AGDA }} --safe EverythingSafe.agda + ${{ env.AGDA }} index.agda - # - name: Golden testing - # run: | - # ${{ env.CABAL_INSTALL }} clock - # make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' + - name: Golden testing + run: | + ${{ env.CABAL_INSTALL }} clock + make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' ######################################################################## @@ -183,7 +183,7 @@ jobs: - name: Deploy HTML uses: JamesIves/github-pages-deploy-action@4.1.3 - # if: ${{ success() && env.AGDA_DEPLOY }} + if: ${{ success() && env.AGDA_DEPLOY }} with: branch: gh-pages From a084ff6149dd4ef2aebb83193da544d33b178e52 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 13 Oct 2023 11:19:47 +0100 Subject: [PATCH 14/18] [ cosmetic ] whitespace --- travis/landing-bottom.html | 3 +-- travis/landing-top.html | 15 +++++++-------- travis/landing.sh | 2 +- 3 files changed, 9 insertions(+), 11 deletions(-) diff --git a/travis/landing-bottom.html b/travis/landing-bottom.html index 9cd52d7c69..941cc8d2b4 100644 --- a/travis/landing-bottom.html +++ b/travis/landing-bottom.html @@ -1,4 +1,3 @@ -
    -
    + diff --git a/travis/landing-top.html b/travis/landing-top.html index 0d214f58b5..ffbb5cebc1 100644 --- a/travis/landing-top.html +++ b/travis/landing-top.html @@ -5,15 +5,14 @@ -
    -

    Development versions

    +

    Development versions

    - + -

    Released versions

    +

    Released versions

    -
      +
        diff --git a/travis/landing.sh b/travis/landing.sh index d3957f558e..062bddceb7 100755 --- a/travis/landing.sh +++ b/travis/landing.sh @@ -8,7 +8,7 @@ cat landing-top.html >> landing.html find html/ -name "index.html" \ | grep -v "master\|experimental" \ | sort -r \ - | sed 's|html/\([^\/]*\)/index.html|
      • \1
        • |g' \ + | sed 's|html/\([^\/]*\)/index.html|
      • \1
        • |g' \ >> landing.html cat landing-bottom.html >> landing.html From e04f06b8aceb28cc05aea2039a6fc83eb33b3f44 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 13 Oct 2023 11:20:23 +0100 Subject: [PATCH 15/18] Revert "[ revert ] go back to building everything" This reverts commit dcc5bb32669a3aa38b7fd39a912b41d748c8b573. --- .github/workflows/ci-ubuntu.yml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 2ecc969589..d8fa5850fe 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -154,13 +154,13 @@ jobs: cabal run GenerateEverything cp travis/* . ./index.sh - ${{ env.AGDA }} --safe EverythingSafe.agda - ${{ env.AGDA }} index.agda + # ${{ env.AGDA }} --safe EverythingSafe.agda + # ${{ env.AGDA }} index.agda - - name: Golden testing - run: | - ${{ env.CABAL_INSTALL }} clock - make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' + # - name: Golden testing + # run: | + # ${{ env.CABAL_INSTALL }} clock + # make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' ######################################################################## @@ -183,7 +183,7 @@ jobs: - name: Deploy HTML uses: JamesIves/github-pages-deploy-action@4.1.3 - if: ${{ success() && env.AGDA_DEPLOY }} + # if: ${{ success() && env.AGDA_DEPLOY }} with: branch: gh-pages From a09366e99381e154330d13de861b22acc0fbdcd3 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 13 Oct 2023 11:20:49 +0100 Subject: [PATCH 16/18] Revert "Revert "[ revert ] go back to building everything"" This reverts commit e04f06b8aceb28cc05aea2039a6fc83eb33b3f44. --- .github/workflows/ci-ubuntu.yml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index d8fa5850fe..2ecc969589 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -154,13 +154,13 @@ jobs: cabal run GenerateEverything cp travis/* . ./index.sh - # ${{ env.AGDA }} --safe EverythingSafe.agda - # ${{ env.AGDA }} index.agda + ${{ env.AGDA }} --safe EverythingSafe.agda + ${{ env.AGDA }} index.agda - # - name: Golden testing - # run: | - # ${{ env.CABAL_INSTALL }} clock - # make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' + - name: Golden testing + run: | + ${{ env.CABAL_INSTALL }} clock + make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' ######################################################################## @@ -183,7 +183,7 @@ jobs: - name: Deploy HTML uses: JamesIves/github-pages-deploy-action@4.1.3 - # if: ${{ success() && env.AGDA_DEPLOY }} + if: ${{ success() && env.AGDA_DEPLOY }} with: branch: gh-pages From f24daec1743e656eb5dbb139d86203d9ffb53646 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 13 Oct 2023 15:46:11 +0100 Subject: [PATCH 17/18] [ cosmetic ] a bit of CSS & logo --- travis/landing-bottom.html | 3 ++- travis/landing-top.html | 20 +++++++++++++------- travis/landing.sh | 3 ++- 3 files changed, 17 insertions(+), 9 deletions(-) diff --git a/travis/landing-bottom.html b/travis/landing-bottom.html index 941cc8d2b4..9cd52d7c69 100644 --- a/travis/landing-bottom.html +++ b/travis/landing-bottom.html @@ -1,3 +1,4 @@ -
      +
    +
    diff --git a/travis/landing-top.html b/travis/landing-top.html index ffbb5cebc1..81b03304b9 100644 --- a/travis/landing-top.html +++ b/travis/landing-top.html @@ -6,13 +6,19 @@ -

    Development versions

    +
    + +

    Documention for the Agda standard library

    - +
    -

    Released versions

    +

    Development versions

    -
      + + +

      Released versions

      + +
        diff --git a/travis/landing.sh b/travis/landing.sh index 062bddceb7..55ebe0c8fb 100755 --- a/travis/landing.sh +++ b/travis/landing.sh @@ -8,9 +8,10 @@ cat landing-top.html >> landing.html find html/ -name "index.html" \ | grep -v "master\|experimental" \ | sort -r \ - | sed 's|html/\([^\/]*\)/index.html|
      • \1
        • |g' \ + | sed 's|html/\([^\/]*\)/index.html|
      • \1
        • |g' \ >> landing.html cat landing-bottom.html >> landing.html mv landing.html html/index.html +mv agda-logo.svg html/ From 223c83c62ab0e91a4a289e018fad89848b0b2cc5 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 13 Oct 2023 15:48:42 +0100 Subject: [PATCH 18/18] [ fix ] missing agda logo --- travis/agda-logo.svg | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 travis/agda-logo.svg diff --git a/travis/agda-logo.svg b/travis/agda-logo.svg new file mode 100644 index 0000000000..0fe434e8ed --- /dev/null +++ b/travis/agda-logo.svg @@ -0,0 +1,16 @@ + + logotype + Created with Sketch. + + + + \ No newline at end of file