8 lines
		
	
	
	
		
			217 B
		
	
	
	
		
			Bash
		
	
	
		
			Executable file
		
	
	
	
	
			
		
		
	
	
			8 lines
		
	
	
	
		
			217 B
		
	
	
	
		
			Bash
		
	
	
		
			Executable file
		
	
	
	
	
| #! /bin/sh
 | |
| #
 | |
| # Some of these should really be done by options to makeinfo or by
 | |
| # using @setfilename, but this way we can have both bashref.info and
 | |
| # bash.info (for installing)
 | |
| #
 | |
| 
 | |
| sed -e 's|bashref.info|bash.info|g'
 | 
