mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-10-30 19:22:31 +00:00 
			
		
		
		
	Docs: Don't READTHEDOCS on local builds
This commit is contained in:
		
							parent
							
								
									8877817fa9
								
							
						
					
					
						commit
						39a1623ac0
					
				
					 1 changed files with 9 additions and 7 deletions
				
			
		|  | @ -16,15 +16,17 @@ html_theme_options: dict[str] = { | |||
|     "source_branch": "main", | ||||
|     "source_directory": "docs/source/", | ||||
| } | ||||
| html_context: dict[str] = {} | ||||
| 
 | ||||
| # try to fix the readthedocs detection | ||||
| html_context: dict[str] = { | ||||
| if os.getenv("READTHEDOCS"): | ||||
|     html_context.update({ | ||||
|         "READTHEDOCS": True, | ||||
|         "display_github": True, | ||||
|         "github_user": "YosysHQ", | ||||
|         "github_repo": "yosys", | ||||
|         "slug": "yosys", | ||||
| } | ||||
|     }) | ||||
| 
 | ||||
| # override source_branch if not main | ||||
| git_slug = os.getenv("READTHEDOCS_VERSION_NAME") | ||||
|  |  | |||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue