#!/bin/bash
# to be sourced by Bash

function lagda () {
  if [ "$*" == "" ]
  then
    find . -name "*.lagda"
  else
    find $* -name "*.lagda"
  fi
}

function agdai () {
  if [ "$*" == "" ]
  then
    find . -name "*.agdai"
  else
    find $* -name "*.agdai"
  fi
}

function noagdai () {
  if [ "$*" == "" ]
  then
    echo svn propset svn:ignore "*.agdai"
  else
    svn propset svn:ignore "*.agdai" $*
  fi
}

export lagda agdai noagdai