diff options
-rw-r--r-- | Makefile.am | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Makefile.am b/Makefile.am index 45807af8b8..deec100c3c 100644 --- a/Makefile.am +++ b/Makefile.am @@ -714,7 +714,6 @@ system_flags = $(foreach system,$(1),-s $(system)) # issue described at <https://savannah.gnu.org/bugs/index.php?51027>. release: dist cd po; git checkout . - cd doc; git checkout . @if ! git diff-index --quiet HEAD; then \ echo "There are uncommitted changes; stopping." >&2 ; \ exit 1 ; \ |