/ ci / push_docs.sh
push_docs.sh
 1  #!/bin/sh
 2  
 3  set -e
 4  
 5  if [ -z "$GH_TOKEN" ] || [ -z "$GH_MAIL" ] || [ -z "$GH_NAME" ]; then
 6    echo "Environment configuration missing, exiting... "
 7    exit 1
 8  fi
 9  
10  TEMP_DIR="temp_$GITHUB_SHA"
11  REPO=$GITHUB_REPOSITORY
12  DOCS_DIR="docs/"
13  
14  # Disable Safe Repository checks
15  git config --global --add safe.directory "/github/workspace"
16  git config --global --add safe.directory "/github/workspace/$TEMP_DIR"
17  
18  # Clone wiki
19  echo "Cloning wiki..."
20  git clone https://$GH_NAME:$GH_TOKEN@github.com/$REPO.wiki.git $TEMP_DIR
21  
22  # Get commit message
23  message=$(git log -1 --format=%B)
24  echo "Message:"
25  echo $message
26  
27  # Copy files
28  echo "Copying files to Wiki"
29  rsync -av --delete $DOCS_DIR $TEMP_DIR/ --exclude .git --exclude-from "$DOCS_DIR/wiki_exclude"
30  
31  # Setup credentials for wiki
32  cd $TEMP_DIR
33  git config user.name $GH_NAME
34  git config user.email $GH_MAIL
35  
36  # Push to Wiki
37  echo "Pushing to Wiki"
38  git add .
39  git commit -m "$message"
40  git push origin master