[linux] /etc/profile opnieuw laden

[Verwijderd]

Hoi,

Stomme vraag misschien... Maar ik heb nogal vaak dat ik even iets moet veranderen in /etc/profile of ~/.bashrc of dergelijke files.

Om de verandering werkend te krijgen moet ik eerst uitloggen en opnieuw inloggen.

Is er geen manier om dit sneller voor elkaar te krijgen?

[2P]

$ source /etc/profile

$ source ~/.bashrc

That will do the job

[Verwijderd]

thanks!

[Tuinhark]

Out of curiousity.. waar is 'source' van? Bij mij staat dat niet op de hd. Of is het een alias die ik niet heb?

[Verwijderd]

Op maandag 03 juni 2002 18:37 schreef Tuinhark het volgende:
Out of curiousity.. waar is 'source' van? Bij mij staat dat niet op de hd. Of is het een alias die ik niet heb?

source hoort bij de bash shell... gebruik je niet toevallig een andere shell dan bash? (csh of zo?)

[kenneth]

source kan ook geen apart programma zijn: anders wordt de environment van de shell zelf niet gewijzigd
(Alleen van het child-process 'source' nl.)
Het moet dus wel een builtin zijn:

code:

$ help source
source: source filename
    Read and execute commands from FILENAME and return.  The pathnames
    in $PATH are used to find the directory containing FILENAME.

[Tuinhark]

Aah.. ik ziet doen. Ik gebruik idd bash, maar wist niet dat het een built-in was. Ik zat ook een beetje te slapen oid toen ik de errormessage zag.. Ik heb em idd gewoon. Vals alarm.