| 
									
										
										
										
											2017-11-06 17:00:25 -07:00
										 |  |  | # Not every platform has or needs sudo, gotta save them O(1)s... | 
					
						
							|  |  |  | sudo_cmd="" | 
					
						
							| 
									
										
										
										
											2017-11-06 18:30:41 -07:00
										 |  |  | set +e | 
					
						
							| 
									
										
										
										
											2017-11-06 18:26:33 -07:00
										 |  |  | if type -p sudo >/dev/null 2>/dev/null; then | 
					
						
							| 
									
										
										
										
											2017-11-06 18:01:40 -07:00
										 |  |  |   ((EUID)) && [[ -z "${ANDROID_ROOT-}" ]] && sudo_cmd="sudo" | 
					
						
							| 
									
										
										
										
											2017-11-06 17:00:25 -07:00
										 |  |  | fi | 
					
						
							| 
									
										
										
										
											2017-11-06 18:30:41 -07:00
										 |  |  | set -e |