mirror of
https://github.com/mudler/LocalAI.git
synced 2024-12-18 12:26:26 +00:00
feat: devcontainer part 4 (#3339)
add utils.sh, prelim docs Signed-off-by: Dave Lee <dave@gray101.com>
This commit is contained in:
parent
6aba6223c7
commit
9cfd89087b
49
.devcontainer-scripts/utils.sh
Normal file
49
.devcontainer-scripts/utils.sh
Normal file
@ -0,0 +1,49 @@
|
|||||||
|
#!/bin/bash
|
||||||
|
|
||||||
|
# This file contains some really simple functions that are useful when building up customization scripts.
|
||||||
|
|
||||||
|
|
||||||
|
# Checks if the git config has a user registered - and sets it up if not.
|
||||||
|
#
|
||||||
|
# Param 1: name
|
||||||
|
# Param 2: email
|
||||||
|
#
|
||||||
|
config_user() {
|
||||||
|
local gcn=$(git config --global user.name)
|
||||||
|
if [ -z "${gcn}" ]; then
|
||||||
|
echo "Setting up git user / remote"
|
||||||
|
git config --global user.name "$1"
|
||||||
|
git config --global user.email "$2"
|
||||||
|
|
||||||
|
fi
|
||||||
|
}
|
||||||
|
|
||||||
|
# Checks if the git remote is configured - and sets it up if not. Fetches either way.
|
||||||
|
#
|
||||||
|
# Param 1: remote name
|
||||||
|
# Param 2: remote url
|
||||||
|
#
|
||||||
|
config_remote() {
|
||||||
|
local gr=$(git remote -v | grep $1)
|
||||||
|
if [ -z "${gr}" ]; then
|
||||||
|
git remote add $1 $2
|
||||||
|
fi
|
||||||
|
git fetch $1
|
||||||
|
}
|
||||||
|
|
||||||
|
# Setup special .ssh files
|
||||||
|
#
|
||||||
|
# Param 1: bash array, filenames relative to the customization directory that should be copied to ~/.ssh
|
||||||
|
setup_ssh() {
|
||||||
|
local files=("$@")
|
||||||
|
for file in "${files[@]}"; then
|
||||||
|
local cfile="/devcontainer-customization/${file}"
|
||||||
|
local hfile="~/.ssh/${file}"
|
||||||
|
if [ ! -f "${hfile}" ]; then
|
||||||
|
echo "copying ${file}"
|
||||||
|
cp "${cfile}" "${hfile}"
|
||||||
|
chmod 600 "${hfile}"
|
||||||
|
fi
|
||||||
|
done
|
||||||
|
ls ~/.ssh
|
||||||
|
}
|
@ -7,14 +7,19 @@ If files with those names exist here, they will be called at the end of the norm
|
|||||||
|
|
||||||
This is a good place to set things like `git config --global user.name` are set - and to handle any other files that are mounted via this directory.
|
This is a good place to set things like `git config --global user.name` are set - and to handle any other files that are mounted via this directory.
|
||||||
|
|
||||||
An example of a useful script might be:
|
To assist in doing so, `source /.devcontainer-scripts/utils.sh` will provide utility functions that may be useful - for example:
|
||||||
|
|
||||||
```
|
```
|
||||||
#!/bin/bash
|
#!/bin/bash
|
||||||
gcn=$(git config --global user.name)
|
|
||||||
if [ -z "$gcn" ]; then
|
source "/.devcontainer-scripts/utils.sh"
|
||||||
git config --global user.name YOUR.NAME
|
|
||||||
git config --global user.email YOUR.EMAIL
|
sshfiles=("config", "key.pub")
|
||||||
git remote add PREFIX FORK_URL
|
|
||||||
fi
|
setup_ssh "${sshfiles[@]}"
|
||||||
|
|
||||||
|
config_user "YOUR NAME" "YOUR EMAIL"
|
||||||
|
|
||||||
|
config_remote "REMOTE NAME" "REMOTE URL"
|
||||||
|
|
||||||
```
|
```
|
Loading…
Reference in New Issue
Block a user