mirror of
https://github.com/paparazzi/paparazzi.git
synced 2026-05-26 16:30:07 +08:00
[supervision] Add settings selector. (#2959)
This commit is contained in:
@@ -18,6 +18,12 @@ PAPARAZZI_HOME = os.getenv("PAPARAZZI_HOME", PAPARAZZI_SRC)
|
||||
CONF_DIR = os.path.join(PAPARAZZI_HOME, "conf/")
|
||||
|
||||
|
||||
def removeprefix(string: str, prefix: str, /) -> str:
|
||||
if string.startswith(prefix):
|
||||
return string[len(prefix):]
|
||||
else:
|
||||
return string[:]
|
||||
|
||||
# TODO: make it work with shell program such as vim.
|
||||
def edit_file(file_path, prefix=CONF_DIR):
|
||||
path = prefix + file_path
|
||||
|
||||
Reference in New Issue
Block a user