The main point was to get rid of the -i option, which just confused my sed.
 Without it, there
is no difference.


On Mon, Mar 17, 2014 at 8:19 PM, Jason Gross <notifications@github.com>wrote:

> In etc/install_coq.sh:
>
> > @@ -23,8 +23,15 @@ git submodule update --init --recursive
> >  pushd coq-HoTT
> >  echo '$ Patching configure'
> >  if [ ! -z "$(grep '\[ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 \]' configure)" ]
> > -then
> > -    sed -i s'/\[ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 \]/[ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 -o "$MAKEVERSIONMAJOR" -gt 3 ]/g' configure
> > +then sed -e 's/\[ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 \]/[ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 -o "$MAKEVERSIONMAJOR" -gt 3 ]/g' \
> > +	 <configure >configure.tmp
>
> Out of curiosity, is there a difference between sed ... <configure and sed
> ... configure?
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/HoTT/HoTT/pull/342/files#r10685574>
> .
>