From 6e8a75f9370c19bc35048be640610bbf1e3d4558 Mon Sep 17 00:00:00 2001
From: halseyj <31658023+halseyj@users.noreply.github.com>
Date: Thu, 6 Dec 2018 22:52:39 +0000
Subject: [PATCH] Update index.md (#24120)

---
 guide/english/linux/index.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/guide/english/linux/index.md b/guide/english/linux/index.md
index be6cea5e32..f258cb7398 100644
--- a/guide/english/linux/index.md
+++ b/guide/english/linux/index.md
@@ -27,7 +27,7 @@ mid 90s. Today, Linux is the most popular operating system in the world. It powe
 Google's popular Android operating system.
 
 There are also many versions of Linux designed to be run on personal computers, such as Debian or Ubuntu. More importantly, these
-different versions of Linux (called distributions) allow the user varying degrees of personalization and control of the operating
+different versions of Linux (called distributions or distros for short) allow the user varying degrees of personalization and control of the operating
 system. This means that users can choose their Linux distributions based on their wants and needs.  
 
 There are Linux distributions which appeal to specific niches, like AVLinux. There are distributions with access to different GUIs and window managers, like Kubuntu or Debian (although you can easily switch between these). There is also Kali Linux which is used for advanced penetration testing and auditing. It has over 700 tools, and to be able to use it efficiently you will need to know how to use the command line. It is not advised for beginners.