diff options
| author | Glenn Morris <rgm@gnu.org> | 2019-05-01 09:15:59 -0700 |
|---|---|---|
| committer | Glenn Morris <rgm@gnu.org> | 2019-05-01 09:15:59 -0700 |
| commit | 3e322df06003e64a491bca47fd14f652374ac3a4 (patch) | |
| tree | d93cf9ad7b8fba9a9fd461b618c9bac8ce52ef73 | |
| parent | ec02c736d65f2fd3a8a17e4e8dc143bf15d9600d (diff) | |
| download | emacs-3e322df06003e64a491bca47fd14f652374ac3a4.tar.gz | |
* admin/update_autogen: Handle git worktree.
; No need to merge to master.
| -rwxr-xr-x | admin/update_autogen | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/admin/update_autogen b/admin/update_autogen index 67ed5d66465..651d35beafb 100755 --- a/admin/update_autogen +++ b/admin/update_autogen @@ -47,7 +47,7 @@ cd $PD cd ../ [ -d admin ] || die "Could not locate admin directory" -[ -d .git ] || die "No .git directory" +[ -e .git ] || die "No .git" usage () { |