Are `ci_scripts/install.sh` and `ci_scripts/push_doc.sh` duplicates / still needed?
Are
ci_scripts/install.shandci_scripts/push_doc.shduplicates / still needed?