Current Linux Release

Debian

The CS Department runs the Debian operating system.

The Dept also has a local package archive which contains odds and ends including backports, unofficial packages and locally made packages.

The current release is 8.0: Jessie

Complete information about this release is available from the Debian website. All department machines are updating nightly, so we run the most recent release with all security fixes.

Linux Kernel Version

All machines run the stock 3.16.0 Debian kernel.

Man pages

If you want to find out how a program works on Linux, the manual program, or man, is your best friend.

To use the manual, type man program, where program is the name of the program you want help on. For example:

man ls
man man

Run man man for more information.

O'Reilly Bookshelf


[| Safari Tech Books Online]

Unlike an online bookstore, Safari Tech Books Online is a fully-searchable e-reference library that houses a vast collection of technical books from industry-leading publishers.

 *Search across the full text of thousands of the best technical books available today.
 *Read books cover to cover online, or flip directly to the answer or code sample you need.
 *Browse books by category to research any technical topic.

Sound in Linux

To listen to online radio stations, such as those on soundcast.com, you will need to use a winamp-like program, xmms. This isn't set as a default for .pls files, so to use this you need to open the .pls file with /usr/bin/xmms.

Xmms can also be used to play cds and other media files.

To edit the sound levels, use the command aumixFAQs for sound related issues

Answers in this category:

Sound doesn't work and I use Gnome

How do I play a CD?

//Author//: mkd@cs.brown.edu

Moving or renaming a file

To move or rename a file, we use the mv command. mv acts exactly like cp, but after making the copy, mv then deletes the original file. Because of this behavior, we can move files and rename them.

For instance, if I'd like to rename file1 to file2, I can do:

mv file1 file2

Or, if I'd like to move a file to my homedirectory, I can do:

mv file ~/

Note: if I don't have permission to remove file from wherever it is, a copy of it will appear in my home directory, but the original won't get deleted (and I will get an error message).

Copying a file in Linux

To copy a file, you should use the cp command. To copy a file from one place to another, you do:

cp SOURCE_FILE DESTINATION_(FILE)

If you give a directory for your destination, it will copy the source_file and put it within that directory with the original file name. Alternatively, if you give a complete path with a file name for the destination, cp will copy the file to the new location, changing its name to the one you supply.

For example, if I have file1 and I want to make a copy named file2, I can do:

cp file1 file2

Or, if I've found a file in someone's directory that I'd like a copy of, I can put it in my home directory with:

cp file ~/

Notice that ~/ translates to "my home directory," and so cp will make a copy of file in my home directory calling it "file". Alternatively, I could name it a bit more informatively:

cp file ~/remember_to_read_this

This will copy file to my home directory and name it remember_to_read_this.

USB mounting in Linux

Under GNOME

If you are using GNOME, your USB storage device will automatically mount when you insert it. An icon for it will appear on your desktop. When you are done using the device, remember to unmount it by right-clicking on the icon and choosing "Unmount."

Important Always unmount your USB device before unplugging it from the system! This protects against file loss and even permanent damage to the device.

Other Window Managers

If you are using a window manager or desktop environment that does not automatically mount USB devices, you must mount them manually using the following commands.

To mount all attached USB devices:

 usbmount -a

To mount a specific USB device (e.g. /dev/sdb1):

 usbmount DEVICE

After mounting a device, you can access the files under the /media directory (the output of usbmount will tell you precisely where to look).

To unmount all mounted USB devices:

 usbumount -a

To unmount a specific USB device:

 usbumount DEVICE

Important Always unmount your USB device before unplugging it from the system! This protects against file loss and even permanent damage to the device.

How to query the installed packages on Debian

The tstaff supported linux machines run the debian distribution, which uses a program called dpkg for package management. To query all packages installed on machine you can run:


dpkg -l


This will return information on the package name, its version, and a quick synopsis of what the package is, for all packages installed on the machine. You can optionally give dpkg a package name, like:


dpkg -l [package name]


and it will return the same information for that single package.

//Author//: mkd@cs.brown.edu

Customizing your desktop environment

Much of this information pertains to old-style accounts which use fvwm. Newer desktop environments, like Gnome, KDE, and Xfce, are much easier to configure.