#! /bin/bash
# Last edited on 2023-02-08 13:09:13 by stolfi

git rm --cache "$@"