Skip to content

Commit 71c8a50

Browse files
Merge branch 'master' into experimental
2 parents b89ecd5 + 7113a58 commit 71c8a50

File tree

315 files changed

+6741
-1010
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

315 files changed

+6741
-1010
lines changed

.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@
1111
*.tix
1212
*.vim
1313
dist
14+
dist-newstyle
1415
Everything.agda
1516
EverythingSafe.agda
1617
EverythingSafeGuardedness.agda

.travis.yml

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -56,8 +56,9 @@ install:
5656
mkdir $HOME/.cabsnap;
5757
cp -a $HOME/.ghc $HOME/.cabsnap/ghc;
5858
cp -a $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin $HOME/installplan.txt $HOME/.cabsnap/;
59-
- cd -
60-
# installing fix-agda-whitespace
59+
# returning to stdlib directory
60+
- cd ../agda-stdlib
61+
# installing fix-whitespace
6162
- git clone https://github.com/agda/fix-whitespace --depth=1
6263
- cd fix-whitespace
6364
- cabal install fix-whitespace.cabal
@@ -89,9 +90,8 @@ script:
8990
# building the docs
9091
- agda $RTS_OPTIONS -i . -i src/ --html safe.agda
9192
- agda $RTS_OPTIONS -i . -i src/ --html index.agda
92-
# moving everything to the experimental directory
93-
- mkdir -p experimental
94-
- mv html/* experimental/
93+
# moving everything to the main directory
94+
- mv html/* .
9595

9696
after_success:
9797
# uploading to gh-pages
@@ -100,10 +100,10 @@ after_success:
100100
- git config --global user.email "[email protected]"
101101
- git remote add upstream https://[email protected]/agda/agda-stdlib.git &>/dev/null
102102
- git fetch upstream && git reset upstream/gh-pages
103-
- git checkout HEAD -- *.html v0.16/ v0.17/ v1.0/ v1.1/ v1.2/
103+
- git checkout HEAD -- *.html v0.16/ v0.17/ v1.0/ v1.1/ v1.2/ experimental/
104104
- git add -f \*.html
105105
- git commit -m "Automatic HTML update via Travis"
106-
- if [ "$TRAVIS_PULL_REQUEST" = "false" ] && [ "$TRAVIS_BRANCH" = "experimental" ];
106+
- if [ "$TRAVIS_PULL_REQUEST" = "false" ] && [ "$TRAVIS_BRANCH" = "master" ];
107107
then git push -q upstream HEAD:gh-pages &>/dev/null;
108108
fi
109109

0 commit comments

Comments
 (0)