Fix the Config with sed
The website moved to a new server and its settings in site/config.ini are out of date. Make every change with sed, not an editor: on real servers you'll often fix files from scripts.
How it works: the terminal below is a real Linux machine running in your browser. Click it and
type. Tasks tick themselves off as you complete them; questions are answered in the box under each task.
Press Reset any time for a fresh machine. Your password on this machine (for
sudo) is student.
Hints
Try each command without -i first and check the output.
Solution explanation
sed -i changes the file directly. The mirror line has two old addresses, so the replacement needs g. Several sed commands can be joined with ;: /^#/d deletes comments and /^$/d deletes empty lines. Without -i, the result goes to the screen, or into a new file with >.
Show solution
cd site
sed -i 's/8080/9090/' config.ini
sed -i 's/debug=true/debug=false/' config.ini
sed -i 's/old-ship.example/new-ship.example/g' config.ini
sed '/^#/d; /^$/d' config.ini > clean.ini
cat clean.ini