Re: doc: Don't leave a broken .texi file around

[Jose E. Marchesi]

Hi Alfred.

> Might as well do it for the other place as well.  Cleans up the
> poke.text target too, the rm / mv stuff is redundant.  
>
> 2022-01-31  Alfred M. Szmidt  <ams@gnu.org>
>
>       * doc/gen-pvm-insns.sh: Try not to use hard coded location for
>       bash.
>
>       * doc/Makefile.am (pvm-insns.texi): Don't create file if the
>       command to create it failed.
>       (poke.text): Remove redundant mv/rm.

Thanks for the patch.  I just applied it to both `master' and
maint/poke-2 on your behalf.

> diff --git a/doc/Makefile.am b/doc/Makefile.am
> index 3bcf5357..4289c22f 100644
> --- a/doc/Makefile.am
> +++ b/doc/Makefile.am
> @@ -24,7 +24,8 @@ EXTRA_DIST = gen-pvm-insns.sh 
> learn-poke-language-in-y-minutes.pk \
>  
>  pvm-insns.texi: $(top_srcdir)/libpoke/pvm.jitter $(srcdir)/gen-pvm-insns.sh
>       $(srcdir)/gen-pvm-insns.sh $(top_srcdir)/libpoke/pvm.jitter \
> -       > pvm-insns.texi
> +       > pvm-insns.texi-tmp
> +     mv pvm-insns.texi-tmp pvm-insns.texi
>  
>  # The documentation for poke settings is generated by poke itself.
>  # This is to avoid replication.  The documentation of the settings
> @@ -76,9 +77,8 @@ pkgdata_DATA += poke.text
>  EXTRA_DIST += poke.text
>  
>  poke.text: $(srcdir)/poke.texi
> -     $(MAKEINFO) --plaintext $(srcdir)/poke.texi > poke.txmp
> -     rm -f $(srcdir)/poke.text
> -     mv poke.txmp $(srcdir)/poke.text
> +     $(MAKEINFO) --plaintext $(srcdir)/poke.texi > poke.text-tmp
> +     mv poke.text-tmp $(srcdir)/poke.text
>  
>  MOSTLYCLEANFILES = \
>    nodelist \
>
> diff --git a/doc/gen-pvm-insns.sh b/doc/gen-pvm-insns.sh
> index 6ac58f16..0e022d4f 100755
> --- a/doc/gen-pvm-insns.sh
> +++ b/doc/gen-pvm-insns.sh
> @@ -1,4 +1,4 @@
> -#!/bin/bash
> +#!/usr/bin/env bash
>  
>  # This program is free software: you can redistribute it and/or modify
>  # it under the terms of the GNU General Public License as published by