Don't duplicate work.
This commit is contained in:
		
							parent
							
								
									a87bf521c8
								
							
						
					
					
						commit
						2b95fb924e
					
				|  | @ -7,3 +7,8 @@ machine: | |||
| test: | ||||
|   override: | ||||
|     - script/proof -f | ||||
| general: | ||||
|   branches: | ||||
|     ignore: | ||||
|       - gh-pages # no proof script here | ||||
|       - master   # don't need to duplicate work | ||||
|  |  | |||
		Loading…
	
		Reference in New Issue