*** Makefile-dist	Tue Jan 25 13:31:56 1994
--- Makefile	Mon Feb  7 22:08:27 1994
***************
*** 63,69 ****
  #
  EXTRADICT = Use_config.sh
  
! SHELL = /bin/sh
  MAKE = make
  
  all:	unpacked
--- 63,69 ----
  #
  EXTRADICT = Use_config.sh
  
! SHELL = /bin/sh -v
  MAKE = make
  
  all:	unpacked
***************
*** 191,197 ****
  		eval $(MAKE) BUILD=$(BUILD) DBUILD=$(DBUILD) CBUILD=$(CBUILD) \
  		  "$$makeargs" $(LANGUAGE_TARGET)  ||  exit 1; \
  		)  ||  exit 1; \
! 		LANGUAGES=`expr "$$LANGUAGES" : '[^{]*{[^}]*}\(.*\)$'`; \
  		case "$$LANGUAGES" in \
  		    ''|*{*}) \
  			;; \
--- 191,197 ----
  		eval $(MAKE) BUILD=$(BUILD) DBUILD=$(DBUILD) CBUILD=$(CBUILD) \
  		  "$$makeargs" $(LANGUAGE_TARGET)  ||  exit 1; \
  		)  ||  exit 1; \
! 		LANGUAGES=`expr "$$LANGUAGES" : '[^{]*{[^}]*}\(.*\)$$'`; \
  		case "$$LANGUAGES" in \
  		    ''|*{*}) \
  			;; \