From 4a80bd98f251ee6040dc6ae453bcbf959dd44d6b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Alexandre=20Delano=C3=AB?= <devel+git@delanoe.org> Date: Tue, 7 May 2019 16:57:19 +0200 Subject: [PATCH] [DEVOPS] folder with scripts to help installation. --- devops/build-doc | 3 +++ debian-install => devops/debian-install | 4 +--- docker-install => devops/docker-install | 0 devops/stats.jq | 1 + 4 files changed, 5 insertions(+), 3 deletions(-) create mode 100755 devops/build-doc rename debian-install => devops/debian-install (99%) rename docker-install => devops/docker-install (100%) create mode 100755 devops/stats.jq diff --git a/devops/build-doc b/devops/build-doc new file mode 100755 index 00000000..79862c51 --- /dev/null +++ b/devops/build-doc @@ -0,0 +1,3 @@ +#!/bin/bash + +stack haddock --no-haddock-deps diff --git a/debian-install b/devops/debian-install similarity index 99% rename from debian-install rename to devops/debian-install index ba381b26..89601218 100755 --- a/debian-install +++ b/devops/debian-install @@ -2,8 +2,6 @@ - - if git --version; then echo "git installed, ok" @@ -12,7 +10,7 @@ else fi sudo apt update -sudo apt install liblzma-dev libpcre3-dev libblas-dev liblapack-dev pkg-config libgsl-dev libbz2-dev postgresql postgresql-server-dev-9.6 +sudo apt install liblzma-dev libpcre3-dev libblas-dev liblapack-dev pkg-config libgsl-dev libbz2-dev postgresql postgresql-server-dev-9.6 nginx #echo "Which user?" #read USER diff --git a/docker-install b/devops/docker-install similarity index 100% rename from docker-install rename to devops/docker-install diff --git a/devops/stats.jq b/devops/stats.jq new file mode 100755 index 00000000..2a942dd6 --- /dev/null +++ b/devops/stats.jq @@ -0,0 +1 @@ +jq < repo.json '.state |= map_values(map_values(length)) | .history |= length' -- 2.21.0