Browse Source

move doc scripts

pull/1261/head
Ivan Schaller 6 months ago
parent
commit
7150e70433
2 changed files with 5 additions and 1 deletions
  1. +0
    -0
      script/build-docs
  2. +5
    -1
      script/get-docs

docs/build_docs.sh → script/build-docs View File


docs/get_docs.py → script/get-docs View File


Loading…
Cancel
Save