-# This adds a special type of git repository, where the .git directory
-# is stored on a file server, to avoid wasting space with it on the client.
-# One example use is storing a music collection in git, where you can spare
-# the extra space needed for .git on your file server, but not on your
-# laptop. This fills basically the same niche as unison.
-#
-# To make mr use this file, add a line like this inside the [DEFAULT]
-# section of your ~/.mrconfig
-#include = cat /usr/share/mr/gitless
-#
-# And an example repo using it would look something like:
-#[lib/sound]
-#checkout = gitless_checkout turtle /media/turtle/home/joey/lib sound
-#
-# In this example, the file server's hostname is "turtle",
-# and it's mounted on /media/turtle. The file server contains a sound.git
-# repository in the specified directory under that mount point.
-# When mr checks out that repository, it will create a sound.hostname
-# directory on the server, containing just the .git directory, and symlink
-# the client's .git directory to it. After checkout, normal git and mr
-# commands can be used, as long as the file server is available.
-
-lib =
- gitless_checkout() {
- server="$1"
- remotebase="$2"
- dir="$3"
- hostname="$(hostname)"
- if [ "$hostname" = "$server" ]; then
- git clone "$dir.git" "$dir"
- else
- if [ ! -d "$remotebase/$dir.$hostname" ]; then
- git clone --no-checkout "$remotebase/$dir.git" "$remotebase/$dir.$hostname"
- fi
- mkdir -p "$dir"
- cd "$dir"
- ln -sf "$remotebase/$dir.$hostname/.git"
- git reset --hard
- fi
- }