profiles: move profiles into a dedicated folder

Tracking these as patches has been causing problems.

Signed-off-by: John Crispin <john@phrozen.org>
This commit is contained in:
John Crispin
2020-09-22 17:57:38 +02:00
parent 49fc316655
commit 35bdbb920b
19 changed files with 228 additions and 362 deletions

View File

@@ -71,6 +71,9 @@ def reset_tree():
["git", "reset", "--hard", config.get("revision", config["branch"])],
check=True,
)
run(
["rm", "-r", "profiles"],
)
print("### Reset done")
except:
print("### Resetting tree failed")
@@ -101,7 +104,9 @@ def setup_tree():
for patch in patches:
run(["git", git_am, "-3", str(base_dir / patch)], check=True)
run(
["ln", "-s", "../profiles"], check=True,
)
print("### Patches done")
except:
print("### Setting up the tree failed")