Skip to content

Commit a35ec23

Browse files
Merge pull request #8890 from dotty-staging/fix-docs
Fix website publishing issue
2 parents 0e25dd9 + 4ded3f9 commit a35ec23

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

project/scripts/genDocs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ echo "Working directory: $PWD"
77
GENDOC_EXTRA_ARGS=$@
88
GIT_HEAD=$(git rev-parse HEAD) # save current head for commit message in gh-pages
99
PREVIOUS_SNAPSHOTS_DIR="$PWD/../prev_snapshots"
10-
SCRIPT_DIR="(cd "$(dirname "${BASH_SOURCE[0]}")" >& /dev/null && pwd)"
10+
SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" >& /dev/null && pwd)"
1111
SITE_OUT_DIR="$PWD/docs/_site"
1212

1313
### Obtain the previous versions of the website ###

0 commit comments

Comments
 (0)