Skip to content
Snippets Groups Projects
Select Git revision
  • a4fd5b669305efa2f00bde535fd198c26cad2d65
  • master default protected
  • feat-create_little_container_for_developer
  • feat/pipeline_publish_extension
  • feat-publish_extension_on_marketplace_with_ci
  • feat-log-in
  • feat-connect_uri_handler_with_chosse_workdir_and_connection
  • feat-choose-mission-workdir
  • 10-en-tant-qu-etudiant-je-souhaite-pouvoir-lancer-une-mission-de-type-vscode-desktop-sur-mon-ide
  • new-building-way-recorder
  • fix-commit-any-challenge-type
  • recorder-push-code
  • theia-extension
  • 0.1.2
  • 0.1.1
  • 0.0.6
  • 1.4
  • 1.3
  • 1.2
  • 1.1
20 results

setup.sh

Blame
    • start.sh 422 B
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    15
    16
    17 
    

    

    

    #!/bin/sh

# setup ssh key for root user
# must be installed by the API first within /tmp/.ssh
mkdir ~/.ssh
cp /tmp/.ssh/* ~/.ssh/

# start command recorder
node deadlock/recorder.js &

deluser theia sudo

su theia --command "python setup_trace.py"
rm setup_trace.py

# starting theia as THEIA
su theia --command "node /home/theia/src-gen/backend/main.js /home/project --hostname=0.0.0.0 --plugins=local-dir:/home/plugins"