Skip to content

Commit ca2e387

Browse files
committed
[ travis ] fix html update (re #1087)
1 parent c36eae9 commit ca2e387

File tree

1 file changed

+2
-3
lines changed

1 file changed

+2
-3
lines changed

.travis.yml

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -90,9 +90,8 @@ script:
9090
# building the docs
9191
- agda $RTS_OPTIONS -i . -i src/ --html safe.agda
9292
- agda $RTS_OPTIONS -i . -i src/ --html index.agda
93-
# moving everything to the experimental directory
94-
- mkdir -p experimental
95-
- mv html/* experimental/
93+
# moving everything to the main directory
94+
- mv html/* .
9695

9796
after_success:
9897
# uploading to gh-pages

0 commit comments

Comments
 (0)