ui.tools.deploy: change article title.
							parent
							
								
									5bb8400d0b
								
							
						
					
					
						commit
						c3dd749f3d
					
				| 
						 | 
					@ -6,8 +6,8 @@ HELP: deploy-tool
 | 
				
			||||||
{ $description "Opens the graphical deployment tool for the specified vocabulary." }
 | 
					{ $description "Opens the graphical deployment tool for the specified vocabulary." }
 | 
				
			||||||
{ $examples { $code "\"tetris\" deploy-tool" } } ;
 | 
					{ $examples { $code "\"tetris\" deploy-tool" } } ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
ARTICLE: "ui.tools.deploy" "Application deployment UI tool"
 | 
					ARTICLE: "ui.tools.deploy" "UI application deployment tool"
 | 
				
			||||||
"The application deployment UI tool provides a graphical front-end to deployment configuration. Using the tool, you can set deployment options graphically."
 | 
					"The application deployment tool provides a graphical front-end to deployment configuration. Using the tool, you can set deployment options graphically."
 | 
				
			||||||
$nl
 | 
					$nl
 | 
				
			||||||
"To start the tool, pass a vocabulary name to a word:"
 | 
					"To start the tool, pass a vocabulary name to a word:"
 | 
				
			||||||
{ $subsections deploy-tool }
 | 
					{ $subsections deploy-tool }
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
		Loading…
	
		Reference in New Issue