Fix manual generation
Grmbl.
This commit is contained in:
		
							parent
							
								
									8cc19ed089
								
							
						
					
					
						commit
						a6ce6d9e7c
					
				
					 1 changed files with 8 additions and 1 deletions
				
			
		|  | @ -42,7 +42,14 @@ let | ||||||
|           export VARTEXFONTS=$TMPDIR/texfonts |           export VARTEXFONTS=$TMPDIR/texfonts | ||||||
|         ''; |         ''; | ||||||
| 
 | 
 | ||||||
|         distPhase = "make dist-gzip; make dist-xz; mkdir -p $out/tarballs; cp *.tar.* $out/tarballs"; |         distPhase = | ||||||
|  |           '' | ||||||
|  |             runHook preDist | ||||||
|  |             make dist-gzip | ||||||
|  |             make dist-xz | ||||||
|  |             mkdir -p $out/tarballs | ||||||
|  |             cp *.tar.* $out/tarballs | ||||||
|  |           ''; | ||||||
| 
 | 
 | ||||||
|         preDist = '' |         preDist = '' | ||||||
|           make -C doc/manual install prefix=$out |           make -C doc/manual install prefix=$out | ||||||
|  |  | ||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue