From 03f43ca6290756514678705676f0655df40eb952 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 31 Jan 2015 17:22:45 -0800 Subject: [PATCH] feat(script): add script for fetching dependencies from https://github.com/leanprover/emacs-dependencies.git --- script/fetch_emacs_deps.sh | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100755 script/fetch_emacs_deps.sh diff --git a/script/fetch_emacs_deps.sh b/script/fetch_emacs_deps.sh new file mode 100755 index 0000000000..39bb866190 --- /dev/null +++ b/script/fetch_emacs_deps.sh @@ -0,0 +1,15 @@ +#!/bin/bash +# Script for copying the Lean Emacs mode dependencies from https://github.com/leanprover/emacs-dependencies.git. +# We usually use it to test `leanemacs` without installing Lean. +# We execute this script at src/emacs. +read -p "Script will delete directory 'dependencies' and create it again with the content of https://github.com/leanprover/emacs-dependencies.git, Are you sure [y/n]? " -n 1 -r +echo # (optional) move to a new line +if [[ ! $REPLY =~ ^[Yy]$ ]] +then + echo "ABORTED." + exit 1 +fi +rm -r -f dependencies +git clone https://github.com/leanprover/emacs-dependencies.git +rm -r -f emacs-dependencies/.git +mv emacs-dependencies dependencies