Skip to content

Instantly share code, notes, and snippets.

@ramntry
Created October 27, 2014 11:57
Show Gist options
  • Select an option

  • Save ramntry/4b999b543e9da3b7980e to your computer and use it in GitHub Desktop.

Select an option

Save ramntry/4b999b543e9da3b7980e to your computer and use it in GitHub Desktop.
#!/bin/bash
if [ -z "$1" ]; then
echo "Usage: $0 <chapter-name>"
exit 1
fi
chapter_name=$1
mkdir $chapter_name
cd $chapter_name
newcoq.sh
emacs *.v &
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment