Commit 2e89fe56 authored by Ansgar Burchardt's avatar Ansgar Burchardt

remove old scripts (unused)

parent 0e9686f2
#!/bin/bash
#
# Clean up left-overs from Docker.
set -e
set -u
docker rm -v $(docker ps -a -q -f status=exited)
docker rmi $(docker images --filter dangling=true -q)
#! /bin/sh
set -e
set -u
logdir="${HOME}/log/$(date +%Y)"
dockerdir="${HOME}/dune-docker"
logfile="${logdir}/$(date +%Y-%m-%d)"
mkdir -p -- "${logdir}"
cd "${dockerdir}"
rm -f dune-git-stamp
make dune-git-stamp > "${logfile}-dune-git" 2>&1
rm -f dune-fufem-git-stamp
make dune-fufem-git-stamp > "${logfile}-dune-fufem-git" 2>&1
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment